1. 'a : S
2. P : 'a
3. x : 'a
4. P(x)
  P(@x:'a. (P(x)))

By:	TAbstract (@x:'a. (P(x)))  THEN Unab [`bchoose`] THEN L Thm* 'a:S, P,Q:('aProp). Thm* (x:'a. Q(x)  P(x))  (x:'a. Q(x))  P(@x:'a. Q(x)) THEN Unab [`so_apply`] THEN Simp THEN StrongAuto

1

x:'a. P(x)

1 step

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