(3steps 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 bool vs decidable fun 1 1
1. A : Type
2. P : AProp
3. x:A. Dec(P(x))
4. x : A
  y:. P(x)  y
By: BackThru: Thm* Dec(P)  (b:. P  b)

Generated subgoals:

None

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

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