pub fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)👎Deprecated:
Seq axioms have been verified, and are now lemmas
Expand description
ensures
#[trigger] (s1 =~= s2)
<==> {
&&& s1.len() == s2.len()
&&& forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
},