Nuprl - Proof: preserved by monotone 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: preserved by monotone 1

1. T : Type
2. P : T

Prop
3. R1 : T

Prop
4. R2 : T

Prop
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)

By:	Using [`x',x] (BackThruSomeHyp THEN EasyHyp)

Generated subgoals:

None

About:

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