---

Step * 1 of Lemma equipollent-union-product


1. A : Type
2. B : Type
3. C : Type
4. a1 : A + B × C@i
5. a2 : A + B × C@i
6. let d,c = a1 
   in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c> 
= let d,c = a2 
  in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c> 
∈ (A × C + (B × C))
⊢ a1 = a2 ∈ (A + B × C)
BY
{ TACTIC:(TACTIC:D -3 THEN D -2 THEN All Reduce) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(TACTIC:D  -3  THEN  D  -2  THEN  All  Reduce)

---

Home Index