---

Step * 1 1 1 of Lemma inject-composes

.....assertion..... 
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))
⊢ ∀x:A. (f x ∈ B1)
BY
{ (Auto THEN DoSubsume THEN Auto) }

---

Latex:


.....assertion..... 
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)
10.  \mforall{}b:B1.  \mforall{}a:B0.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
\mvdash{}  \mforall{}x:A.  (f  x  \mmember{}  B1)


By

(Auto  THEN  DoSubsume  THEN  Auto)

---

Home Index