Function lemma_iset_remove_insert Copy item path

s.contains(a),

(#[trigger] s.remove(a)).insert(a) == s,

Removing an element a from a set s and then inserting a back into the set is equivalent to the original sets`.