(3steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subset squash exteq 1 1

1. A : Type
2. P : AProp
  x:AP(x P(x)


By: Rewrite by Thm*  P  P


Generated subgoals:

None

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

(3steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc