(7steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star closure 1

1. T : Type
2. R : TTProp
3. R2 : TTProp
4. Trans(T)(R2(_1,_2))
5. x,y:T. (x R y (x R2 y)
6. x : T
7. y : T
8. x R^0 y
  (x R2 y x = y


By: ReduceExp -1 THEN SimpConcl


Generated subgoals:

None

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

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