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