Function lemma_sorted_unique

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.

Function lemma_sorted_uniqueCopy item path