Data Nat:* = O:Nat | S:(k:Nat)Nat;

General Y;

genplus:(m:Nat)(n:Nat)Nat;
by Y;
intro PLUS m n;
induction m;
fill n;
intros;
fill S (PLUS k n);
Qed;

undefined:(A:*)A;
by Y;
intro UNDEF A;
refine UNDEF;
Qed;
Freeze undefined;

Data List (A:*) : * = nil:List A | cons:(x:A)(xs:List A)List A;

head:(A:*)(xs:List A)A;
intros;
induction xs;
refine undefined;
intros;
refine x;
Qed;

Eval head _ (cons _ O (nil Nat));
Eval head _ (nil Nat);