---

Step * of Lemma equipollent-union-product

∀[A,B,C:Type].  A + B × C ~ A × C + (B × C)
BY
{ TACTIC:(Auto
          THEN TACTIC:(Auto
                       THEN With ⌜λp.let d,c = p 
                                     in case d of inl(a) => inl <a, c> | inr(b) => inr <b, c> ⌝ (D 0)⋅
                       THEN Auto
                       THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)))
          ) }

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

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

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    A  +  B  \mtimes{}  C  \msim{}  A  \mtimes{}  C  +  (B  \mtimes{}  C)


By

---

Latex:
TACTIC:(Auto
                THEN  TACTIC:(Auto
                                          THEN  With  \mkleeneopen{}\mlambda{}p.let  d,c  =  p 
                                                                      in  case  d  of  inl(a)  =>  inl  <a,  c>  |  inr(b)  =>  inr  <b,  c>  \mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  Auto
                                          THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))
                )

---

Home Index