Inductive nat : Type :=  O : nat | S : nat -> nat.
Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.
Inductive tree (A : Type) : Type :=
    leaf : tree A | node : A -> tree A -> tree A -> tree A.
Inductive itree (A B : Type) : Type :=
    ileaf : itree A B | inode : A -> (B -> itree A B) -> itree A B.

Print nat_ind.
Print list_ind.
Print tree_ind.
Print itree_ind.

Variable A B X : Type.

Fixpoint natR f g n : X := match n with 
   O => f | S p => g p (natR f g p) 
end.
Check natR.

Fixpoint listR f g (l:list A) : X := match l with 
   nil => f | cons a p => g a p (listR f g p) 
end.
Check listR.

Fixpoint treeR f g (t:tree A) : X := match t with 
   leaf => f | node a l r => g a l r (treeR f g l) (treeR f g r)
end.
Check treeR.

Fixpoint itreeR f g (t: itree A B) : X := match t with 
   ileaf => f | inode a F => g a F (fun x => itreeR f g (F x))
end.
Check itreeR.