(18steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc bool vs decidable 1
1. P : Prop
  Dec(P)  (b:. P  b)
By: 2 Times Analyze

Generated subgoals:

1 2. Dec(P)
  b:. P  b
7 steps
2 2. b:. P  b
  Dec(P)
9 steps

About:
boolassertdecidablepropexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(18steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc