---

Step * of Lemma only-two-bools

∀f:⋂T:Type. (T ⟶ T ⟶ T). ((f = (λx,y. x) ∈ (⋂T:Type. (T ⟶ T ⟶ T))) ∨ (f = (λx,y. y) ∈ (⋂T:Type. (T ⟶ T ⟶ T))))
BY
{ (InstLemma `polymorphic-choice` [] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:\mcap{}T:Type.  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  T).  ((f  =  (\mlambda{}x,y.  x))  \mvee{}  (f  =  (\mlambda{}x,y.  y)))


By

---

Latex:
(InstLemma  `polymorphic-choice`  []  THEN  Auto)

---

Home Index