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