proposition: Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.
proof: Proof. unfold In; split. - intros (e',H). destruct (eq_dec x y) as [E|E]; auto. right; exists e'; auto. apply (add_3 E H). - destruct (eq_dec x y) as [E|E]; auto. + intros. exists e; apply add_1; auto. + intros [H|(e',H)]. * destruct E; auto. * exists e'; apply add_2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface