Nuprl - Proof: comp preserves inj 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp preserves inj 1 1 1

1. B : Type
2. A : Type
3. C : Type
4. g : A

B
5. f : B

C
6.

a1,a2:A. g(a1) = g(a2)

a1 = a2
7.

b1,b2:B. f(b1) = f(b2)

b1 = b2
8. a1 : A
9. a2 : A
10. f(g(a1)) = f(g(a2))

g(a1) = g(a2)

By:	BackThru: Hyp:7

Generated subgoals:

None

About:

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