vars a,b: Type

generated type Set a ::= empty | add a (Set a)

generated type Sys b ::= node b (Set (Sys b))

type Nat

var a: Type

generated type CTree a ::= leaf a | branch (Nat ->? CTree a)

free type L ::= abs (L -> L)

free type Tree a b ::= leaf b | branch (a -> Tree a b)

free type List a ::= nil | cons (a; List a)

var b : Type

op map : (a -> b) -> List a -> List b

free type Tree a b ::= leaf a | branch (b -> List (Tree a b))

var c : Type

op fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

op __ o __ : (b -> c) * (a -> b) -> a -> c

vars f : a -> c; g : (b -> List c) -> c; x : a; s : b -> List (Tree a b)

. fold f g (leaf x) = f x

. def (fold f g (branch s))

. fold f g (branch s) = g (map (fold f g) o s)

var Q : Pred(Set (Sys b)); P : Pred (Sys b)

. (forall x : b; s : Set (Sys b) . Q s => P (node x s))

/\ Q empty

/\ (forall s : Set (Sys b); t : Sys b . Q s /\ P t => Q (add t s))

=> forall t : Sys b . P t

var R : Pred(CTree a)

. (forall x : a . R (leaf x))

/\ (forall f : Nat ->? CTree a .

(forall x : Nat . def f x => R (f x)) => R (branch f))

=> forall t : CTree a . R t