Step
*
of Lemma
isatom2-bool-if-has-value
∀[t:Base]. isatom2(t) ∈ 𝔹 supposing (t)↓
BY
{ CanonicalAuto }
Latex:
Latex:
\mforall{}[t:Base].  isatom2(t)  \mmember{}  \mBbbB{}  supposing  (t)\mdownarrow{}
By
Latex:
CanonicalAuto
Home
Index