proposition: Lemma bal_bindings l x e r : bindings (bal l x e r) = bindings (create l x e r).
proof: Proof. functional induction (bal l x e r); intros; cleanf; auto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)