---

Step * 1 of Lemma equipollent-union-sum


1. A : Type
2. B : Type
3. C : A ⟶ Type
4. D : B ⟶ Type
5. a1 : a:A × C[a] + (b:B × D[b])@i
6. a2 : a:A × C[a] + (b:B × D[b])@i
7. case a1 of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>
= case a2 of inl(p) => let a,c = p in <inl a, c> | inr(p) => let b,d = p in <inr b , d>
∈ (d:A + B × case d of inl(a) => C[a] | inr(b) => D[b])
⊢ a1 = a2 ∈ (a:A × C[a] + (b:B × D[b]))
BY
{ TACTIC:(DProdsAndUnions
          THEN All Reduce
          THEN (EqHD (-1) THENA Auto)
          THEN All Reduce
          THEN Try ((ImpossibleEq Auto (-2) THEN Auto))
          THEN RepeatFor 2 ((EqCD THENA Auto))
          THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(DProdsAndUnions
                THEN  All  Reduce
                THEN  (EqHD  (-1)  THENA  Auto)
                THEN  All  Reduce
                THEN  Try  ((ImpossibleEq  Auto  (-2)  THEN  Auto))
                THEN  RepeatFor  2  ((EqCD  THENA  Auto))
                THEN  Auto)

---

Home Index