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

At: compose inject
A,B,C:Type, f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f)
By:
Unfold `inject` 0
THEN
Reduce 0
Generated subgoal:

11. 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		1 step

About:
functionuniverseequalimpliesall

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