---

Step * of Lemma poly-choice-eta-2

∀f:Base. ((∀x,y:Base.  ((f x y) = x ∈ Base)) ⇒ (f ~ λx.if f x is lambda then λy.x otherwise ⊥))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert (f 0)↓ BY
               ((Assert (f 0 0)↓ BY (Subst' (f 0 0) = 0 ∈ Base 0 THEN Auto)) THEN HasValueD (-1) THEN Auto))
   THEN (CallByValueApplyCases (-1) THENA Auto)
   THEN Try (((Assert f (λx.x) ≤ ⊥ BY
                     ((InstHyp [⌜λx.x⌝] (-1)⋅ THENA (Auto THEN RepUR ``has-value`` 0 THEN Auto))
                      THEN Reduce (-1)
                      THEN Auto))
              THEN (Assert f (λx.x) (λx.x) ≤ ⊥ (λx.x) BY
                          Auto)
              THEN (RWO "2" (-1) THENA Auto)
              THEN (Subst' ⊥ (λx.x) ~ ⊥ -1 THENA (Strictness THEN Auto))
              THEN (InstLemma `not_id_sqeq_bottom` [] THEN Auto)
              THEN D -1
              THEN SqequalSqle
              THEN Auto))
   THEN HypSubst' (-1) 0
   THEN EqCD
   THEN Reduce 0) }

1
1. f : Base@i
2. ∀x,y:Base.  ((f x y) = x ∈ Base)
3. (f 0)↓
4. f ~ λx.(f x)
5. x : Base
⊢ f x ~ if f x is lambda then λy.x otherwise ⊥

---

Latex:

---

Latex:
\mforall{}f:Base.  ((\mforall{}x,y:Base.    ((f  x  y)  =  x))  {}\mRightarrow{}  (f  \msim{}  \mlambda{}x.if  f  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  (f  0)\mdownarrow{}  BY
                          ((Assert  (f  0  0)\mdownarrow{}  BY  (Subst'  (f  0  0)  =  0  0  THEN  Auto))  THEN  HasValueD  (-1)  THEN  Auto))
  THEN  (CallByValueApplyCases  (-1)  THENA  Auto)
  THEN  Try  (((Assert  f  (\mlambda{}x.x)  \mleq{}  \mbot{}  BY
                                      ((InstHyp  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  RepUR  ``has-value``  0  THEN  Auto))
                                        THEN  Reduce  (-1)
                                        THEN  Auto))
                        THEN  (Assert  f  (\mlambda{}x.x)  (\mlambda{}x.x)  \mleq{}  \mbot{}  (\mlambda{}x.x)  BY
                                                Auto)
                        THEN  (RWO  "2"  (-1)  THENA  Auto)
                        THEN  (Subst'  \mbot{}  (\mlambda{}x.x)  \msim{}  \mbot{}  -1  THENA  (Strictness  THEN  Auto))
                        THEN  (InstLemma  `not\_id\_sqeq\_bottom`  []  THEN  Auto)
                        THEN  D  -1
                        THEN  SqequalSqle
                        THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  EqCD
  THEN  Reduce  0)

---

Home Index