(2steps total) PrintForm Definitions Lemmas hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: not exists 1
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)
THEN
StrongAuto

Generated subgoals:

None

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

(2steps total) PrintForm Definitions Lemmas hol Sections HOLlib Doc