proposition: Lemma bal_mapsto l x e r y e' : MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r).
proof: Proof. functional induction (bal l x e r); intros; cleanf; unfold assert_false, create; intuition_m. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)