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