1 2 3 4 5
Definition NIL := (Nil nat). Type <(List nat)>Cases (Nil nat) of NIL => NIL | _ => NIL end.