lemma_prefix_of_common_sequence

vstd_extra::seq_extra

Function lemma_prefix_of_common_sequence 

Source 
pub proof fn lemma_prefix_of_common_sequence(
    source1: Seq<nat>,
    source2: Seq<nat>,
    child: Seq<nat>,
)
Expand description
requires
source1.is_prefix_of(child),
source2.is_prefix_of(child),
ensures
source1 == source2 || source1.len() < source2.len() && source1.is_prefix_of(source2)
    || source2.len() < source1.len() && source2.is_prefix_of(source1),

If source1 and source2 are prefixes of child, then either source1 is equal to source2 or one of them is a prefix of the other.