proposition: Lemma remove_remove_redundant : forall elt k fmap, Equal (@remove elt k (remove k fmap)) (remove k fmap).
proof: Proof. intros; apply remove_notIn_Equal. eauto using remove_1, E.eq_refl. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils