proposition: Lemma add_remove_cancel: forall (elt : Type) (k k' : key) (v : elt) (m : t elt), k = k' -> Equal ([k |> v] :: remove k' m) ([k |> v] :: m).
proof: Proof. intros. rewrite Equal_mapsto_iff. intros *; map_iff; intuition (subst; tauto). Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils