---

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

.....assertion..... 
∀x,y:Base.  (eval z = x in λy.z y ~ x)
BY
{ (Intros THEN SqequalSqle THEN AssumeHasValue) }

1
1. x : Base
2. y : Base
3. (eval z = x in λy.z y)↓
⊢ eval z = x in λy.z y ≤ x

2
1. x : Base
2. y : Base
3. is-exception(eval z = x in λy.z y)
⊢ eval z = x in λy.z y ≤ x

3
1. x : Base
2. y : Base
3. (x)↓
⊢ x ≤ eval z = x in λy.z y

4
1. x : Base
2. y : Base
3. is-exception(x)
⊢ x ≤ eval z = x in λy.z y

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}x,y:Base.    (eval  z  =  x  in  \mlambda{}y.z  y  \msim{}  x)


By

---

Latex:
(Intros  THEN  SqequalSqle  THEN  AssumeHasValue)

---

Home Index