---

Step * 2 of Lemma equipollent-function-product


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : C ⟶ A × (C ⟶ B)@i
⊢ ∃a:C ⟶ (A × B). (<λx.(fst((a x))), λx.(snd((a x)))> = b ∈ (C ⟶ A × (C ⟶ B)))
BY
{ (D (-1) THEN With ⌜λx.<b1 x, b2 x>⌝ (D 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  :  C  {}\mrightarrow{}  A  \mtimes{}  (C  {}\mrightarrow{}  B)@i
\mvdash{}  \mexists{}a:C  {}\mrightarrow{}  (A  \mtimes{}  B).  (<\mlambda{}x.(fst((a  x))),  \mlambda{}x.(snd((a  x)))>  =  b)


By

---

Latex:
(D  (-1)
  THEN  With  \mkleeneopen{}\mlambda{}x.<b1  x,  b2  x>\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto)

---

Home Index