test-suite/failure/Case14.v


1
2
3
4
5
6
7
8

Inductive List [A:Set] :Set := 
 Nil:(List A) | Cons:A->(List A)->(List A).

Definition NIL := (Nil nat).
Type <(List nat)>Cases (Nil nat) of 
                NIL   => NIL
              |  _    => NIL
              end.