A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u))  Prop

By:	Guarding (n:. <prop>) Auto THEN CompNatInd Concl THEN UnivCD

1

1. A : Type 2. P : AProp 3. n :  4. n1:. n1<n  (X:(A^n1). ( u in X: A^n1. P(u))  Prop) 5. X : A^n   ( u in X: A^n. P(u))  Prop

11 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html