(14steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel inverse exp 2

1. T : Type
2. R : TTProp
3. n : 
4. 0<n
5. x,y:T. (x R^n-1^-1 y (x R^-1^n-1 y)
  x,y:T. (x R^n^-1 y (x R^-1^n y)


By: Unfold `rel_inverse` 0 THEN Reduce 0 THEN Fold `rel_inverse` 0


Generated subgoals:

1 6. x : T
7. y : T
8. y R^n x
  x R^-1^n y

6 steps
2 6. x : T
7. y : T
8. x R^-1^n y
  y R^n x

5 steps

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

(14steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc