"If the composition of two functions is injective, then the right function is injective."
[[T :type] [U :type] [V :type]
[f (==> U V)] [g (==> T U)]]
(==> (injective (compose f g))
(assume [Hc (injective (compose f g))
x T y T
Hi (equal (g x) (g y))]
(have <a> (equal (f (g x)) (f (g y))) :by (e/eq-cong f Hi))
(have <b> (equal ((compose f g) x) ((compose f g) y)) :by <a>)
(have <c> (equal x y) :by (Hc x y <b>)))
"(Hc x y <b>) takes instances x,y of type T, and the codomain equality"