---

Step * 1 1 of Lemma strong-subtype-b-union


1. A : Type
2. B : Type
3. ¬A ⋂ B
4. strong-subtype(A ⋂ B;Void)
⊢ strong-subtype(A ⋂ B;B)
BY
{ (UseTrans ⌜Void⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \mneg{}A  \mcap{}  B
4.  strong-subtype(A  \mcap{}  B;Void)
\mvdash{}  strong-subtype(A  \mcap{}  B;B)


By

---

Latex:
(UseTrans  \mkleeneopen{}Void\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index