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. g(a) = b
  a:A. f(g(a)) = c

1

11. a : A 12. g(a) = b   f(g(a)) = c

1 step

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