Function vstd::seq::axiom_seq_ext_equal

source · 
pub broadcast proof fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
Expand description
ensures
#[trigger] (s1 =~= s2)
    <==> {
        &&& s1.len() == s2.len()
        &&& forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]

    },