Function vstd::seq::axiom_seq_ext_equal_deep

source · 
pub broadcast proof fn axiom_seq_ext_equal_deep<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]

    },