proposition: Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m).
proof: Proof. unfold In. split; intros (e0,H0); exists e0. - apply (MapsTo_1 H H0); auto. - apply (MapsTo_1 (E.eq_sym H) H0); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface