proposition: Lemma treeify_zero_rb : treeify_rb_invariant 0 0 (@treeify_zero elt).
proof: Proof. intros acc _; simpl; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)