proposition: Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m.
proof: Proof. unfold In; split. - intros (e,H). split. + assert (In y (remove x m)) by (exists e; auto). intro H1; apply (remove_1 H1 H0). + exists e; apply remove_3 with x; auto. - intros (H,(e,H0)); exists e; apply remove_2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface