(7steps total) PrintForm Definitions mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable-exists-finite
  T:Type, P:(TProp). (x:T. Dec(P(x)))  finite-type(T)  Dec(x:T. P(x))
By: Auto

Generated subgoal:

1 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. finite-type(T)
  Dec(x:T. P(x))
6 steps

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

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