Nuprl - Proof: rel plus trans

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel plus trans

T:Type, R:(T

Prop). Trans x,y:T. x R^+ y

By:	Unfold `trans` 0 THEN All (Unfold `rel_plus`) THEN All Reduce THEN ExRepD THEN InstConcl [n1+n]

Generated subgoal:

1 1. T : Type
2. R : TTProp
3. a : T
4. b : T
5. c : T
6. n1 :
7. a R^n1 b
8. n :
9. b R^n c
a R^n1+n c
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html