Nuprl - Proof: compose bij 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose bij 1

1. T : Type
2. f : T

T
3. g : T

T
4.

a1,a2:T. f(a1) = f(a2)

a1 = a2
5.

b:T.

a:T. f(a) = b
6.

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

a1 = a2
7.

b:T.

a:T. g(a) = b
8. a1 : T
9. a2 : T
10. f(g(a1)) = f(g(a2))

a1 = a2

By:	BackThru -5 THEN EasyHyp

Generated subgoals:

None

About:

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