Nuprl - Proof: same range sep eqv 1 3

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: same range sep eqv 1 3

1. A : Type
2. B : Type
3. u : A

B
4. v : A

B
5.

j:B. (

i:A. u(i) = j)

(

i:A. v(i) = j)
6. z : A

B
7.

j:B. (

i:A. v(i) = j)

(

i:A. z(i) = j)

j:B. (

i:A. u(i) = j)

(

i:A. z(i) = j)

By:	Rewrite by Hyp:-1

Generated subgoals:

None

About:

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