---

Step * 1 1 of Lemma equipollent-union-product


1. A : Type
2. B : Type
3. C : Type
4. a3 : A + B@i
5. a4 : C@i
6. a5 : A + B@i
7. a6 : C@i
8. case a3 of inl(a) => inl <a, a4> | inr(b) => inr <b, a4> 
= case a5 of inl(a) => inl <a, a6> | inr(b) => inr <b, a6> 
∈ (A × C + (B × C))
⊢ <a3, a4> = <a5, a6> ∈ (A + B × C)
BY
{ ((D 4 THEN D 6) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  a3  :  A  +  B@i
5.  a4  :  C@i
6.  a5  :  A  +  B@i
7.  a6  :  C@i
8.  case  a3  of  inl(a)  =>  inl  <a,  a4>  |  inr(b)  =>  inr  <b,  a4> 
=  case  a5  of  inl(a)  =>  inl  <a,  a6>  |  inr(b)  =>  inr  <b,  a6> 
\mvdash{}  <a3,  a4>  =  <a5,  a6>


By

---

Latex:
((D  4  THEN  D  6)  THEN  All  Reduce  THEN  Auto)

---

Home Index