test-suite/success/induct.v


1
2
3
4
5
6
7
8
9
10

(* Teste des definitions inductives imbriquees *)

Require PolyList.

Inductive X : Set := 
    cons1 : (list X)->X.

Inductive Y : Set := 
    cons2 : (list Y*Y)->Y.