pub fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)👎Deprecated:
Seq axioms have been verified, and are now lemmas
Expand description
ensures
#[trigger] s1.add(s2).len() == s1.len() + s2.len(),