Function vstd::seq::axiom_seq_len_decreases

source · 
pub proof fn axiom_seq_len_decreases<A>(s1: Seq<A>, s2: Seq<A>)
Expand description
requires
s2.len() < s1.len(),
forall |i2: int| {
    0 <= i2 < s2.len() && #[trigger] trigger(s2[i2])
        ==> exists |i1: int| 0 <= i1 < s1.len() && s1[i1] == s2[i2]
},
ensures
decreases_to!(s1 => s2),