---

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


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
BY
{ ((Assert ⌜b ~ (λp.(snd(p))) <ff, b>⌝⋅ THEN Reduce 0 THEN Auto)
   THEN HypSubst' -1 0
   THEN HypSubst' -1 -2
   THEN Thin (-1)
   THEN ImageTypeInduction⋅
   THEN Auto) }

1
1. A : Type
2. B : Type
3. a : A
4. b : B
5. ¬A ⋂ B
6. a1 : Base
7. b1 : Base
8. (λp.(snd(p))) a1 ∈ B
9. a1 = b1 ∈ (x:𝔹 × if x then A else B fi )
⊢ ((λp.(snd(p))) a1) = ((λp.(snd(p))) b1) ∈ B

---

Latex:

---

Latex:

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:
((Assert  \mkleeneopen{}b  \msim{}  (\mlambda{}p.(snd(p)))  <ff,  b>\mkleeneclose{}\mcdot{}  THEN  Reduce  0  THEN  Auto)
  THEN  HypSubst'  -1  0
  THEN  HypSubst'  -1  -2
  THEN  Thin  (-1)
  THEN  ImageTypeInduction\mcdot{}
  THEN  Auto)

---

Home Index