---

Step * 1 of Lemma b-union-equality-disjoint

.....assertion..... 
1. A : Type
2. B : Type
3. a : A
4. b : B
5. ¬A ⋂ B
6. a = b ∈ (A ⋃ B)
⊢ a = b ∈ B
BY
{ (Unfold `b-union` (-1) THEN Unfold `tunion` -1) }

1
1. A : Type
2. B : Type
3. a : A
4. b : B
5. ¬A ⋂ B
6. a = b ∈ Image((x:𝔹 × if x then A else B fi ),(λp.(snd(p))))
⊢ a = b ∈ B

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  a  :  A
4.  b  :  B
5.  \mneg{}A  \mcap{}  B
6.  a  =  b
\mvdash{}  a  =  b


By

---

Latex:
(Unfold  `b-union`  (-1)  THEN  Unfold  `tunion`  -1)

---

Home Index