fact: Definition treeify_cont (f g : treeify_t) : treeify_t := fun acc => match f acc with | (l, x::acc) => match g acc with | (r, acc) => (Bk l x r, acc) end | _ => bogus end.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat