---

Step * of Lemma is-list-if-has-value-rec_wf

∀[t:Base]. (is-list-if-has-value-rec(t) ∈ ℙ)
BY
{ (Auto THEN RepUR ``is-list-if-has-value-rec`` 0 THEN MemCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (is-list-if-has-value-rec(t)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  RepUR  ``is-list-if-has-value-rec``  0  THEN  MemCD  THEN  Auto)

---

Home Index