proposition: Lemma add_in : forall m x y e, In y (add x e m) <-> X.eq y x \/ In y m.
proof: Proof. intros m x y e; functional induction (add x e m); auto; intros; try (rewrite bal_in, IHt); intuition_in. apply In_1 with x; auto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int