fact: Definition treeify_invariant size (f:treeify_t) := forall acc, size <= length acc -> let (t,acc') := f acc in cardinal t = size /\ acc = elements t ++ acc'.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat