pub fn axiom_seq_push_index_same<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] == a,