---

Step * 1 of Lemma polymorphic-choice-sq


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
⊢ (f ~ λx.if f x is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)
BY
{ UseWitness ⌜if f 0 1=0 then tt else ff⌝⋅ }

1
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
⊢ if f 0 1=0 then tt else ff ∈ (f ~ λx.if f x is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)

---

Latex:

---

Latex:

1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
\mvdash{}  (f  \msim{}  \mlambda{}x.if  f  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  \mvee{}  (f  \msim{}  \mlambda{}x,y.  y)


By

---

Latex:
UseWitness  \mkleeneopen{}if  f  0  1=0  then  tt  else  ff\mkleeneclose{}\mcdot{}

---

Home Index