Nuprl - Proof: compose bij 2

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

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. b : T

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

By:	InstHyp [b] -4 THEN ExRepD

Generated subgoal:

1 9. a : T
10. f(a) = b
a:T. f(g(a)) = b
3 steps

About:

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