proposition: Lemma treeify_one_rb : treeify_rb_invariant 1 0 (@treeify_one elt).
proof: Proof. intros [|(x,e) acc]; simpl; autom; inversion 1. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)