T:Type, P:(TProp), R:(TTProp). R preserves P  R^* preserves P

1

1. T : Type 2. P : TProp 3. R : TTProp 4. x,y:T. P(x)  (x R y)  P(y) 5. x : T 6. y : T 7. P(x) 8. x (R^*) y   P(y)

7 steps

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