(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 1
1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. finite-type(T)
  Dec(x:T. P(x))
By: Analyze -1 THEN ExRepD THEN Assert ((x:T. P(x))  (i:n. P(f(i))))

Generated subgoals:

1 4. n : 
5. f : nT
6. Surj(n; T; f)
  (x:T. P(x))  (i:n. P(f(i)))
4 steps
2 4. n : 
5. f : nT
6. Surj(n; T; f)
7. (x:T. P(x))  (i:n. P(f(i)))
  Dec(x:T. P(x))
1 step

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