(8steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-decidable-set
  T:Type, P:(TProp).
  (x:T. Dec(P(x)))
  
  (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))
By: UnivCD
THEN
RWO
Thm* P:(TProp). 
Thm* (x:T. SqStable(P(x)))
Thm* 
Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))
0
THEN
RepeatFor 2 (Analyze 0)

Generated subgoals:

1 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. L:T List. x:T. P(x)  (x  L)
  L:T List. x:T. P(x)  (x  L)
1 step
2 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. L:T List. x:T. P(x)  (x  L)
  L:T List. x:T. P(x)  (x  L)
6 steps

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

(8steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc