Nuprl - Proof: unicomp assoc 1 1

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

1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. f : A

B
6. g : B

C
7. h : C

D
8. x : A

(h o g o f)(x) = (h o g o f)(x)

By:	Compute Co(h o g o f)(x) Co* Coh((g o f)(x)) * h(g(f(x))) * (h o g)(f(x)) * (h o g o f)(x)

Generated subgoals:

None

About:

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