---

Step * 2 1 of Lemma equipollent-product-sum


1. [A] : Type
2. [B] : A ⟶ Type
3. [C] : a:A ⟶ B[a] ⟶ Type
4. f : a:A ⟶ B[a]
5. b1 : x:A ⟶ C[x;f x]
⊢ ∃a:x:A ⟶ (y:B[x] × C[x;y]). (<λx.(fst((a x))), λx.(snd((a x)))> = <f, b1> ∈ (f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])))
BY
{ (With ⌜λx.<f x, b1 x>⌝ (D 0)⋅ THEN Reduce 0 THEN Auto THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [C]  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  Type
4.  f  :  a:A  {}\mrightarrow{}  B[a]
5.  b1  :  x:A  {}\mrightarrow{}  C[x;f  x]
\mvdash{}  \mexists{}a:x:A  {}\mrightarrow{}  (y:B[x]  \mtimes{}  C[x;y]).  (<\mlambda{}x.(fst((a  x))),  \mlambda{}x.(snd((a  x)))>  =  <f,  b1>)


By

---

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

---

Home Index