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

1

9. b : B 10. f(b) = c   a:A. f(g(a)) = c

3 steps

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