Nuprl - Proof: hexists def 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hexists def 1 1 1 1 1

1. 'a : S
2. P : 'a

x:'a. P(x)

P(@x:'a. (P(x)))

By:	Inst Thm* 'a:S, P,Q:('aProp). Thm* (x:'a. Q(x) P(x)) (x:'a. Q(x)) P(@x:'a. Q(x)) ['a;x.P(x);x.P(x)] THEN Unab [`so_apply`] THEN All Reduce THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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