---

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

.....assertion..... 
1. A : Type
2. B : Type
3. strong-subtype(A ⋂ B;B)
4. A ⊆r (A ⋃ B)
5. b : B
6. a : A
7. b = a ∈ (A ⋃ B)
⊢ b = a ∈ A
BY
{ (Unfold `b-union` (-1)
   THEN Unfold `tunion` -1
   THEN (Assert ⌜a ~ (λp.(snd(p))) <tt, a>⌝⋅ THEN Reduce 0 THEN Auto)
   THEN HypSubst' -1 0
   THEN HypSubst' -1 -2
   THEN Thin (-1)
   THEN (ImageTypeInduction⋅ THENA Auto))⋅ }

1
1. A : Type
2. B : Type
3. strong-subtype(A ⋂ B;B)
4. A ⊆r (A ⋃ B)
5. b : B
6. a : A
7. a1 : Base
8. b1 : Base
9. (λp.(snd(p))) a1 ∈ A
10. a1 = b1 ∈ (x:𝔹 × if x then A else B fi )
⊢ ((λp.(snd(p))) a1) = ((λp.(snd(p))) b1) ∈ A

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  strong-subtype(A  \mcap{}  B;B)
4.  A  \msubseteq{}r  (A  \mcup{}  B)
5.  b  :  B
6.  a  :  A
7.  b  =  a
\mvdash{}  b  =  a


By

---

Latex:
(Unfold  `b-union`  (-1)
  THEN  Unfold  `tunion`  -1
  THEN  (Assert  \mkleeneopen{}a  \msim{}  (\mlambda{}p.(snd(p)))  <tt,  a>\mkleeneclose{}\mcdot{}  THEN  Reduce  0  THEN  Auto)
  THEN  HypSubst'  -1  0
  THEN  HypSubst'  -1  -2
  THEN  Thin  (-1)
  THEN  (ImageTypeInduction\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index