proposition: Lemma join_bindings l x d r : Ok (create l x d r) -> bindings (join l x d r) = bindings (create l x d r).
proof: Proof. unfold create at 1. join_tac l x d r; trivial. - simpl in *. invok. rewrite create_bindings. now apply add_below_bindings. - clear Hlr. factornode l. invok. rewrite create_bindings. now apply add_above_bindings. - clear Hrl LT. factornode r. invok; invlt. rewrite bal_bindings, !create_bindings, bindings_node. rewrite <- app_assoc; simpl. f_equal. f_equal. now rewrite Hlr, create_bindings by (ok; intuition). - clear Hlr LT LT'. factornode l. invok; invlt. rewrite bal_bindings, !create_bindings, bindings_node. now rewrite Hrl, create_bindings, <- app_assoc by (ok; intuition). Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)