---

Step * of Lemma polymorphic-constant-bool

∀f:⋂A:Type. (A ⟶ 𝔹). ∃t:𝔹. ∀A:Type. ∀x:A.  f x = t
BY
{ (Auto THEN BLemma `polymorphic-constant` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  \mBbbB{}).  \mexists{}t:\mBbbB{}.  \mforall{}A:Type.  \mforall{}x:A.    f  x  =  t


By

---

Latex:
(Auto  THEN  BLemma  `polymorphic-constant`  THEN  Auto)

---

Home Index