Nuprl - Proof: rel star monotone

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

T:Type, R1,R2:(T

Prop). R1 => R2

R1^* => R2^*

By:	Unfolds [`rel_star`;`rel_implies`] 0 THEN Reduce 0 THEN ParallelOp -1 THEN MoveToConcl -1 THEN MoveToConcl -2 THEN MoveToConcl -2 THEN All (Fold `rel_implies`)

Generated subgoal:

1 1. T : Type
2. R1 : TTProp
3. R2 : TTProp
4. R1 => R2
5. n :
R1^n => R2^n
1 step

About:

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