---

Step * of Lemma equipollent-function-function

∀[A,B,C:Type].  A ⟶ B ⟶ C ~ (A × B) ⟶ C
BY
{ (Auto
   THEN ((Auto THEN With ⌜λf,p. let a,b = p in f a b⌝ (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 : A ⟶ B ⟶ C
5. a2 : A ⟶ B ⟶ C
6. (λp.let a,b = p in a1 a b) = (λp.let a,b = p in a2 a b) ∈ ((A × B) ⟶ C)
⊢ a1 = a2 ∈ (A ⟶ B ⟶ C)

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. b : (A × B) ⟶ C
⊢ ∃a:A ⟶ B ⟶ C. ((λp.let a@0,b = p in a a@0 b) = b ∈ ((A × B) ⟶ C))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((Auto  THEN  With  \mkleeneopen{}\mlambda{}f,p.  let  a,b  =  p  in  f  a  b\mkleeneclose{}  (D  0)\mcdot{})
              THEN  Auto
              THEN  RepeatFor  2  (D  0)
              THEN  Reduce  0
              THEN  Auto)
  )

---

Home Index