---

Step * of Lemma is-atomic_wf

∀[x:Value()]. (is-atomic(x) ∈ 𝔹)
BY
{ (ProveWfLemma THEN D (-1)) }

1
1. x : Base
2. (x)↓
⊢ if x is a pair then ff otherwise if x is inl then ff
                                   else if x is inr then ff
                                        else tt ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}[x:Value()].  (is-atomic(x)  \mmember{}  \mBbbB{})


By

---

Latex:
(ProveWfLemma  THEN  D  (-1))

---

Home Index