(2steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc exteq gfun2 1
1. A : Type
2. P : AProp
3. B : x:AType(given P(x))
  B  {u:A| P(u) }Type
By: BackThru: Thm* P:(AProp). {x:A| P(x) }Prop =ext x:AProp(given P(x))

Generated subgoals:

None

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

(2steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc