---

Step * of Lemma bool-to-dcdr-aux

∀[A:Type]. ∀f:A ⟶ 𝔹. ∀x:A.  Dec(f x = tt)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:A.    Dec(f  x  =  tt)


By

---

Latex:
Auto

---

Home Index