---

Step * of Lemma itermMinus-num_wf

∀[v:int_term()]. itermMinus-num(v) ∈ int_term() supposing ↑itermMinus?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:int\_term()].  itermMinus-num(v)  \mmember{}  int\_term()  supposing  \muparrow{}itermMinus?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index