proposition: Lemma bindings_node r l o : bindings (Node l o r) = (List.map (fstmap xO) (bindings l)) ++ (match o with Some e => (1,e)::nil | None => nil end) ++ (List.map (fstmap xI) (bindings r)).
proof: Proof. unfold bindings at 1. simpl. rewrite !xbindings_alt, !app_nil_r. destruct o; simpl; try f_equal. rewrite xbindings_alt; simpl. f_equal. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)