---

Step * of Lemma inject-composes

∀[A,B0,B1,C:Type]. ∀[f:A ─→ B0]. ∀[g:B1 ─→ C].
  (Inj(A;C;g o f)) supposing (Inj(B1;C;g) and Inj(A;B0;f) and strong-subtype(B0;B1))
BY
{ Auto }

1
1. A : Type
2. B0 : Type
3. B1 : Type
4. C : Type
5. f : A ─→ B0
6. g : B1 ─→ C
7. strong-subtype(B0;B1)
8. Inj(A;B0;f)
9. Inj(B1;C;g)
⊢ Inj(A;C;g o f)

---

Latex:


\mforall{}[A,B0,B1,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B0].  \mforall{}[g:B1  {}\mrightarrow{}  C].
    (Inj(A;C;g  o  f))  supposing  (Inj(B1;C;g)  and  Inj(A;B0;f)  and  strong-subtype(B0;B1))


By

Auto

---

Home Index