proposition: Lemma remove_add_cancel: forall (elt : Type) (k k' : key) (v : elt) (m : t elt), k ∉ m -> k = k' -> Equal (remove k' ([k |> v] :: m)) m.
proof: Proof. intros. rewrite Equal_mapsto_iff. intros *; map_iff. destruct (E.eq_dec k' k0); msubst; intuition subst; repeat match goal with | _ => progress msubst | _ => progress intuition | [ H: MapsTo _ _ _ |- _ ] => learn (MapsTo_In H) end. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils