fact: Definition treeify_invariant size (f:treeify_t) := forall acc, size <= length acc -> let (m,acc') := f acc in cardinal m = size /\ acc = bindings m ++ acc'.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)