proposition: Lemma remove_add_comm: forall (elt : Type) (k k' : M.key) (v' : elt) (m : M.t elt), not (E.eq k k') -> Equal (remove k (add k' v' m)) (add k' v' (remove k 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. eauto using E.eq_trans, E.eq_sym. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils