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

By:	Compute Co( u in X: A^n. P(u) Co(* Co(n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u)))) Co Prop

1

(n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u))))    Prop

10 steps

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