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