data C -> cobTree(A, B) = debTree: C -> A + (B * (C * C)). def fold_cobTree{B0: A -> C, B1: B * (C * C) -> C}: cobTree(A, B) * (nat * C) -> C = (t, (n, c)) => fn ( t , {| zero: () => (fn: _ => c) | succ: f => (fn: t => { b0 a => B0 a | b1 (b, (t1, t2)) => B1 (b, (fn (t1, f), fn (t2, f))) } debTree t ) |} n ).