---

Step * of Lemma strong-subtype_functionality

∀[A1,B1,A2,B2:Type].  (A1 ≡ A2 ⇒ B1 ≡ B2 ⇒ strong-subtype(A1;B1) ⇒ strong-subtype(A2;B2))
BY
{ (Unfold `strong-subtype` 0 THEN Auto) }

1
1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. A1 ≡ A2@i
6. B1 ≡ B2@i
7. (A1 ⊆r B1) c∧ ({b:B1| ∃a:A1. (b = a ∈ B1)}  ⊆r A1)@i
8. A2 ⊆r B2
⊢ {b:B2| ∃a:A2. (b = a ∈ B2)}  ⊆r A2

---

Latex:

---

Latex:
\mforall{}[A1,B1,A2,B2:Type].    (A1  \mequiv{}  A2  {}\mRightarrow{}  B1  \mequiv{}  B2  {}\mRightarrow{}  strong-subtype(A1;B1)  {}\mRightarrow{}  strong-subtype(A2;B2))


By

---

Latex:
(Unfold  `strong-subtype`  0  THEN  Auto)

---

Home Index