---

Step * 1 of Lemma inject-composes


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)
BY
{ (FLemma `strong-subtype-implies` [-3] THENA 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)
10. ∀b:B1. ∀a:B0.  ((b = a ∈ B1) ⇒ (b = a ∈ B0))
⊢ Inj(A;C;g o f)

---

Latex:



1.  A  :  Type
2.  B0  :  Type
3.  B1  :  Type
4.  C  :  Type
5.  f  :  A  {}\mrightarrow{}  B0
6.  g  :  B1  {}\mrightarrow{}  C
7.  strong-subtype(B0;B1)
8.  Inj(A;B0;f)
9.  Inj(B1;C;g)
\mvdash{}  Inj(A;C;g  o  f)


By

(FLemma  `strong-subtype-implies`  [-3]  THENA  Auto)

---

Home Index