Nuprl - Proof: comp preserves inj 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp preserves inj 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 o g)(a1) = (f o g)(a2)

a1 = a2

By:	Reduce Hyp:10

Generated subgoal:

1 10. f(g(a1)) = f(g(a2))
a1 = a2
2 steps

About:

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