Function vstd::seq_lib::lemma_no_dup_in_concat
source · pub proof fn lemma_no_dup_in_concat<A>(a: Seq<A>, b: Seq<A>)Expand description
requires
a.no_duplicates(),b.no_duplicates(),forall |i: int, j: int| 0 <= i < a.len() && 0 <= j < b.len() ==> a[i] != b[j],#[trigger] (a + b).no_duplicates(),If sequences a and b don’t have duplicates, and there are no elements in common between them, then the concatenated sequence a + b will not contain duplicates either.