(*
*)

Inductive dlist : Set -> Type :=
| dnil : forall A:Set, dlist A
| dcons : forall A:Set, A -> dlist A -> dlist (A*A).

Inductive flist (A:Set) : Set :=
| fnil : flist A
| fcons : A -> flist (A->A) -> flist A.


Require Import List.

Inductive ltree : Set :=
    node : list ltree -> ltree.
Check ltree_ind.
Eval compute in ltree_ind.

(*Scheme tree_i := Induction for ltree Sort Prop 
with forest_i := Induction for list Sort Prop.
*)

(*
Inductive ftree : Set :=
    fnode : flist ftree -> ftree.

Inductive list’ (A:Set) : Set :=
| nil’ : list’ A
| cons’ : A -> list’ A -> list’ (A*A).
*)

Inductive Bad : Set :=
   bad : (Bad -> Bad) -> Bad.


Definition badbad (b:Bad) : Bad :=
  match b with bad f => f (f b) end.

badbad (bad badbad) --> badbad (badbad (bad badbad)) --> ...