proposition: Lemma treeify_one_spec : treeify_invariant 1 (@treeify_one elt).
proof: Proof. intros [|x acc]; simpl; auto. inversion 1. destruct x. simpl; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)