Function vstd::seq_lib::lemma_sorted_unique

source · 
pub proof fn lemma_sorted_unique<A>(x: Seq<A>, y: Seq<A>, leq: FnSpec<(A, A), bool>)
Expand description
requires
sorted_by(x, leq),
sorted_by(y, leq),
total_ordering(leq),
x.to_multiset() == y.to_multiset(),
ensures
x =~= y,

Any two sequences that are sorted by a total order and that have the same elements are equal.