(5steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable ex unit 2 1
1. P : UnitProp
2. Dec(P())
  Surj(1; Unit; x.)
By: Unfold `surject` 0 THEN Reduce 0 THEN InstConcl [0]

Generated subgoal:

1 3. b : Unit
   = b
1 step

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

(5steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc