---

Step * 1 of Lemma equipollent-function-function


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)
BY
{ (RepeatFor 2 ((Ext THEN Auto))
   THEN (ApFunToHypEquands `Z' ⌜Z <x, x1>⌝ ⌜C⌝ (-3)⋅ THENA Auto)⋅
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  a1  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
5.  a2  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
6.  (\mlambda{}p.let  a,b  =  p  in  a1  a  b)  =  (\mlambda{}p.let  a,b  =  p  in  a2  a  b)
\mvdash{}  a1  =  a2


By

---

Latex:
(RepeatFor  2  ((Ext  THEN  Auto))
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  <x,  x1>\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)\mcdot{}
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index