Function lemma_update_is_remove_insert

Source
pub broadcast proof fn lemma_update_is_remove_insert<A>(s: Seq<A>, i: int, a: A)
Expand description
requires
0 <= i < s.len(),
ensures
#[trigger] s.update(i, a) =~= s.remove(i).insert(i, a),

Lemma showing that update is equivalent to a remove followed by an insertae