---

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

.....antecedent..... 
1. A : Type
2. B : Type
3. ¬A ⋂ B
4. strong-subtype(A ⋂ B;Void)
5. strong-subtype(A;A ⋃ B)
⊢ strong-subtype(B;B ⋃ A)
BY
{ (BLemma `strong-subtype-b-union-better` THEN Auto)⋅ }

1
1. A : Type
2. B : Type
3. ¬A ⋂ B
4. strong-subtype(A ⋂ B;Void)
5. strong-subtype(A;A ⋃ B)
⊢ strong-subtype(B ⋂ A;A)

---

Latex:

---

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


By

---

Latex:
(BLemma  `strong-subtype-b-union-better`  THEN  Auto)\mcdot{}

---

Home Index