---

Step * of Lemma equipollent-function-product

∀[A,B,C:Type].  C ⟶ (A × B) ~ C ⟶ A × (C ⟶ B)
BY
{ (Auto
   THEN ((Auto THEN With ⌜λf.<λx.(fst((f x))), λx.(snd((f x)))>⌝ (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 : C ⟶ (A × B)@i
5. a2 : C ⟶ (A × B)@i
6. <λx.(fst((a1 x))), λx.(snd((a1 x)))> = <λx.(fst((a2 x))), λx.(snd((a2 x)))> ∈ (C ⟶ A × (C ⟶ B))@i
⊢ a1 = a2 ∈ (C ⟶ (A × B))

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((Auto  THEN  With  \mkleeneopen{}\mlambda{}f.<\mlambda{}x.(fst((f  x))),  \mlambda{}x.(snd((f  x)))>\mkleeneclose{}  (D  0)\mcdot{})
              THEN  Auto
              THEN  RepeatFor  2  (D  0)
              THEN  Reduce  0
              THEN  Auto)
  )

---

Home Index