Function vstd::seq_lib::seq_to_set_is_finite

source · 
pub broadcast proof fn seq_to_set_is_finite<A>(seq: Seq<A>)
Expand description
ensures
#[trigger] seq.to_set().finite(),

The set obtained from a sequence is finite