---

Step * 2 of Lemma equipollent-union-function


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : A ⟶ C × (B ⟶ C)@i
⊢ ∃a:(A + B) ⟶ C. (<λa@0.(a (inl a@0)), λb.(a (inr b ))> = b ∈ (A ⟶ C × (B ⟶ C)))
BY
{ (D -1
   THEN With ⌜λd.case d of inl(x) => b1 x | inr(x) => b2 x⌝ (D 0)⋅
   THEN Reduce 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN Ext⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  b  :  A  {}\mrightarrow{}  C  \mtimes{}  (B  {}\mrightarrow{}  C)@i
\mvdash{}  \mexists{}a:(A  +  B)  {}\mrightarrow{}  C.  (<\mlambda{}a@0.(a  (inl  a@0)),  \mlambda{}b.(a  (inr  b  ))>  =  b)


By

---

Latex:
(D  -1
  THEN  With  \mkleeneopen{}\mlambda{}d.case  d  of  inl(x)  =>  b1  x  |  inr(x)  =>  b2  x\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  Ext\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index