T:Type, P:(TProp), R1,R2:(TTProp).
  (x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P

1

1. T : Type 2. P : TProp 3. R1 : TTProp 4. R2 : TTProp 5. x,y:T. (x R1 y)  (x R2 y) 6. x,y:T. P(x)  (x R2 y)  P(y) 7. x : T 8. y : T 9. P(x) 10. x R1 y   P(y)

1 step

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