---

Step * 2 of Lemma equipollent-union-product


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : A × C + (B × C)@i
⊢ ∃a:A + B × C. (let d,c = a in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c>  = b ∈ (A × C + (B × C)))
BY
{ RepeatFor 2 (D -1) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. x1 : A@i
5. x2 : C@i
⊢ ∃a:A + B × C. (let d,c = a in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c>  = (inl <x1, x2>) ∈ (A × C + (B × \000CC)))

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. y1 : B@i
5. y2 : C@i
⊢ ∃a:A + B × C. (let d,c = a in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c>  = (inr <y1, y2> ) ∈ (A × C + (B ×\000C C)))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  b  :  A  \mtimes{}  C  +  (B  \mtimes{}  C)@i
\mvdash{}  \mexists{}a:A  +  B  \mtimes{}  C.  (let  d,c  =  a  in  case  d  of  inl(a)  =>  inl  <a,  c>  |  inr(b)  =>  inr  <b,  c>    =  b)


By

---

Latex:
RepeatFor  2  (D  -1)

---

Home Index