1. A : Type
2. B : Type
3. C : Type
4. g : AB
5. f : BC
6. b:B. a:A. g(a) = b
7. c:C. b:B. f(b) = c
8. c : C
9. b : B
10. f(b) = c
11. a : A
12. g(a) = b
  f(g(a)) = c

By:	Rewrite by g(a) = b  B

None

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