(21steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no finite model 1
1. A : Type
2. R : AAProp
3. A
4. Trans x,y:A. R(x;y)
5. x:A. y:A. R(x;y)
6. Finite(A)
  x:A. R(x;x)
By: Inst: 
Thm*  R:(AAProp). 
Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
Thm*  
Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))
Using:[A | R]

Generated subgoal:

1 7. k:. f:(kA). i,j:k. i<j  R(f(i);f(j))
  x:A. R(x;x)
15 steps

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

(21steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc