Function vstd::seq_lib::lemma_seq_contains
source · pub proof fn lemma_seq_contains<A>(s: Seq<A>, x: A)Expand description
ensures
s.contains(x) <==> exists |i: int| 0 <= i < s.len() && s[i] == x,