IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not all1 1. T:S, P:(T). (x:T. P(x)) (x:T. P(x))
T:S, P:(TProp). (x:T. P(x)) (x:T. P(x))
By:
(RepeatMFor 2 (Analyze 0)) THEN (Unab [`so_apply`])
THEN
(InstHyp [T;x.(P(x))] 1)
THEN
Simp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:S, P:(T
). 
(
(
x:T. 
x.
(P(x))] 1)
