proposition: Lemma add_in m x y e : y ∈ (add x e m) <-> y == x \/ y ∈ m.
proof: Proof. functional induction (add x e m); auto; intros; cleanf; rewrite ?bal_in; intuition_in. setoid_replace y with x; auto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)