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