A:Type, B:(AType), P:(x:AB(x)Prop).
  (x:A. !y:B(x). P(x,y))  (!f:(x:AB(x)). x:A. P(x,f(x)))

By:	SimilarTo: Thm*  (x:A. !y:B(x). P(x,y))  (f:(x:AB(x)). x:A. P(x,f(x)))

1

1. A : Type 2. B : AType 3. P : x:AB(x)Prop 4. x:A. !y:B(x). P(x,y) 5. f : x:AB(x) 6. x:A. P(x,f(x))   f is the f:(x:AB(x)). x:A. P(x,f(x))

6 steps

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