proposition: Lemma bal_in l x e r y : y ∈ (bal l x e r) <-> y == x \/ y ∈ l \/ y ∈ r.
proof: Proof. unfold In. setoid_rewrite bal_mapsto. unfold create. setoid_rewrite node_mapsto. firstorder. exists e; firstorder. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)