Function vstd::set::axiom_set_difference_finite

source · 
pub broadcast proof fn axiom_set_difference_finite<A>(s1: Set<A>, s2: Set<A>)
Expand description
requires
s1.finite(),
ensures
#[trigger] s1.difference(s2).finite(),

The set difference between two finite sets is finite.