Function vstd::set_lib::lemma_subset_equality

source · 
pub proof fn lemma_subset_equality<A>(x: Set<A>, y: Set<A>)
Expand description
requires
x.subset_of(y),
x.finite(),
y.finite(),
x.len() == y.len(),
ensures
x =~= y,

If x is a subset of y and the size of x is equal to the size of y, x is equal to y.