---

Step * of Lemma injection-if-compose-injection

∀[T:Type]. ∀[f,g:T ⟶ T].  Inj(T;T;f) supposing Inj(T;T;g o f)
BY
{ (Auto THEN All (RepUR ``inject compose``)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f,g:T  {}\mrightarrow{}  T].    Inj(T;T;f)  supposing  Inj(T;T;g  o  f)


By

---

Latex:
(Auto  THEN  All  (RepUR  ``inject  compose``)\mcdot{}  THEN  Auto)

---

Home Index