proposition: Lemma treeify_zero_spec : treeify_invariant 0 (@treeify_zero elt).
proof: Proof. intro. simpl. auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)