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