Nuprl - Proof: equiv rel self functionality 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: equiv rel self functionality 1 1 1

1. T : Type
2. R : T

Prop
3.

a:T. R(a,a)
4.

a,b:T. R(a,b)

R(b,a)
5.

a,b,c:T. R(a,b)

R(b,c)

R(a,c)
6. a : T
7. a' : T
8. b : T
9. b' : T
10. R(a,b)
11. R(a',b')
12. R(a,a')

R(b,b')

By:	(FwdThru 4 [10]) THEN (FwdThru 5 [13;12]) THEN (FwdThru 5 [14;11])

Generated subgoals:

None

About:

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