proposition: Lemma remove_neq_in_iff : forall m x y, ~ E.eq x y -> (In y (remove x m) <-> In y m).
proof: Proof. split; intros (e',H0); exists e'. - apply (remove_3 H0). - apply remove_2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface