(* Let's define an infinite tree whose nodes are made of natural value and an *)
(* infinite forest of infinite trees whose nodes ...                          *)

(* (obbrobrio_tree n) is used to build such a tree whose root value is n and *)
(* root forest is made of the corecursively defined tress whose roots values *)
(* are (n+1), (n+2), ...                                                     *)

(* To finish, we provide also some destructors and a funny (?!?) theorem     *)

CoInductive tree : Set :=
   node : nat -> forest -> tree      
with forest : Set :=
   nil : forest
 | cons : tree -> forest -> forest.

CoFixpoint obbrobrio_tree : nat -> tree :=
 [n:nat]
  (node n (obbrobrio_forest (S n) nil))
with obbrobrio_forest : nat -> forest -> forest :=
 [n:nat][f:forest]
  (cons (obbrobrio_tree n) (obbrobrio_forest (S n) f)).

Definition root_value : tree -> nat :=
 [t:tree]
 Cases t of
    (node n _) => n
 end.

Definition root_forest : tree -> forest :=
 [t:tree]
 Cases t of
    (node _ f) => f
 end.

Definition root_tree : forest -> tree :=
 [f:forest]
 Cases f of
    nil => (obbrobrio_tree (S (S (S O))))
  | (cons t _) => t
 end.

Theorem easy : (root_value (root_tree (root_forest (obbrobrio_tree O))))=(S O).
Proof.
 Trivial.
Qed.