IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
negnegelim imp notfin imp unb inf11 1. P:Prop. PP 2. A : Type
3. (n:. A ~ n)
(0 injA)
By:
Witness: x.x THEN Analyze THEN Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
P:Prop. 
P
n:
. A ~ 
(
A)
x.x THEN Analyze THEN Analyze
