---

Step * of Lemma has-value-length-member-int

∀[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓
BY
{ (InstLemma `length-wf-has-value` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  ||l||  \mmember{}  \mBbbZ{}  supposing  (||l||)\mdownarrow{}


By

---

Latex:
(InstLemma  `length-wf-has-value`  []  THEN  Trivial)

---

Home Index