pub fn axiom_seq_push_index_different<A>(s: Seq<A>, a: A, i: int)👎Deprecated:
Seq axioms have been verified, and are now lemmas
Expand description
requires
i < s.len(),#[trigger] s.push(a)[i] == s[i],