(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 1
1. P : UnitProp
2. Dec(P())
3. x : Unit
  Dec(P(x))
By: Analyze -1 THEN Fold `it` 0

Generated subgoals:

None

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