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