Nuprl - Proof: same range sep inj eqv 1 2

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

1. A : Type
2. B : Type
3. (A inj

B)
4. u : A inj

B
5. v : A inj

B
6.

j:B. (

i:A. u(i) = j)

(

i:A. v(i) = j)

j:B. (

i:A. v(i) = j)

(

i:A. u(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