'a:S, P,Q:('aProp).
  (x:'a. Q(x)  P(x))  ((x:'a. Q(x))  (x:'a. P(x)))  P(@x:'a. Q(x))

1

1. 'a : S 2. P : 'aProp 3. Q : 'aProp 4. x:'a. Q(x)  P(x) 5. (x:'a. Q(x))  (x:'a. P(x))   P(InjCase(lem({x:'a| Q(x) }); x. x, arb('a)))

7 steps

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