T:Type, R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y)

By:	Auto THEN AssertBY R1^* => R2^* (BackThru Thm* R1,R2:(TTProp). R1 => R2  R1^* => R2^*) THEN Unfold `rel_implies` -1 THEN BackThru -1

None

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