(2steps total) PrintForm graph 1 1 Sections Graphs Doc

At: compose inject 1
1. A: Type
2. B: Type
3. C: Type
4. f: AB
5. g: BC
6. a1,a2:A. f(a1) = f(a2) a1 = a2
7. a1,a2:B. g(a1) = g(a2) a1 = a2
8. a1: A
9. a2: A
10. g(f(a1)) = g(f(a2))
a1 = a2
By: Obvious
Generated subgoals:

None

About:
applyfunctionuniverseequalimpliesall

(2steps total) PrintForm graph 1 1 Sections Graphs Doc