---

Step * of Lemma not-poly-choice-eta-2

¬(∀f:Base. ((∀x,y:Base.  ((f x y) = x ∈ Base)) ⇒ (f ~ λx,y. (f x y))))
BY
{ Assert ⌜∀x,y:Base.  (eval z = x in λy.z y ~ x)⌝⋅ }

1
.....assertion..... 
∀x,y:Base.  (eval z = x in λy.z y ~ x)

2
1. ∀x,y:Base.  (eval z = x in λy.z y ~ x)
⊢ ¬(∀f:Base. ((∀x,y:Base.  ((f x y) = x ∈ Base)) ⇒ (f ~ λx,y. (f x y))))

---

Latex:

---

Latex:
\mneg{}(\mforall{}f:Base.  ((\mforall{}x,y:Base.    ((f  x  y)  =  x))  {}\mRightarrow{}  (f  \msim{}  \mlambda{}x,y.  (f  x  y))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x,y:Base.    (eval  z  =  x  in  \mlambda{}y.z  y  \msim{}  x)\mkleeneclose{}\mcdot{}

---

Home Index