---

Step * 1 of Lemma compose-injections


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
BY
{ (BackThruSomeHyp' THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  Inj(T;T;f)
4.  g  :  T  {}\mrightarrow{}  T
5.  Inj(T;T;g)
6.  a1  :  T@i
7.  a2  :  T@i
8.  (f  (g  a1))  =  (f  (g  a2))@i
\mvdash{}  a1  =  a2


By

---

Latex:
(BackThruSomeHyp'  THEN  Auto)

---

Home Index