vstd::seq_lib

Function 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