---

Step * of Lemma compose-injections

∀[T:Type]. ∀[f,g:{f:T ⟶ T| Inj(T;T;f)} ].  (f o g ∈ {f:T ⟶ T| Inj(T;T;f)} )
BY
{ (Auto THEN MemTypeCD THEN Auto THEN D 0 THEN Auto THEN D 2 THEN D 4 THEN Reduce (-1)) }

1
1. T : Type
2. f : T ⟶ T
3. Inj(T;T;f)
4. g : T ⟶ T
5. Inj(T;T;g)
6. a1 : T@i
7. a2 : T@i
8. (f (g a1)) = (f (g a2)) ∈ T@i
⊢ a1 = a2 ∈ T

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  D  0  THEN  Auto  THEN  D  2  THEN  D  4  THEN  Reduce  (-1))

---

Home Index