---

Step * of Lemma isatom1-bool-if-has-value

∀[t:Base]. isatom1(t) ∈ 𝔹 supposing (t)↓
BY
{ CanonicalAuto }

---

Latex:

---

Latex:
\mforall{}[t:Base].  isatom1(t)  \mmember{}  \mBbbB{}  supposing  (t)\mdownarrow{}


By

---

Latex:
CanonicalAuto

---

Home Index