---

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


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
BY
{ ((InstLemma `pair-eta` [⌜a1⌝]⋅ THENA Auto)
   THEN HypSubst (-1) (-2)
   THEN HypSubst (-1) 0
   THEN Thin (-1)
   THEN (InstLemma `pair-eta` [⌜b1⌝]⋅ THENA Auto)
   THEN HypSubst (-1) (-2)
   THEN HypSubst (-1) 0
   THEN Thin (-1)
   THEN Reduce 0)⋅ }

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. <fst(a1), snd(a1)> = <fst(b1), snd(b1)> ∈ (x:𝔹 × if x then A else B fi )
⊢ (snd(a1)) = (snd(b1)) ∈ A

---

Latex:

---

Latex:

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.  a1  :  Base
8.  b1  :  Base
9.  (\mlambda{}p.(snd(p)))  a1  \mmember{}  A
10.  a1  =  b1
\mvdash{}  ((\mlambda{}p.(snd(p)))  a1)  =  ((\mlambda{}p.(snd(p)))  b1)


By

---

Latex:
((InstLemma  `pair-eta`  [\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst  (-1)  (-2)
  THEN  HypSubst  (-1)  0
  THEN  Thin  (-1)
  THEN  (InstLemma  `pair-eta`  [\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst  (-1)  (-2)
  THEN  HypSubst  (-1)  0
  THEN  Thin  (-1)
  THEN  Reduce  0)\mcdot{}

---

Home Index