(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. P : UnitProp
2. Dec(P())
  finite-type(Unit)
By: Unfold `finite-type` 0 THEN InstConcl [1;x.]

Generated subgoal:

1   Surj(1; Unit; x.)
2 steps

About:
decidableunititnatural_numberlambdafunctionprop
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