---

Step * of Lemma ml-length_wf

∀[T:Type]. ∀[l:T List]. (ml-length(l) ∈ ℕ) supposing valueall-type(T)
BY
{ (InstLemma `ml-length-sq` [] THEN RepeatFor 3 (ParallelLast') THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  (ml-length(l)  \mmember{}  \mBbbN{})  supposing  valueall-type(T)


By

---

Latex:
(InstLemma  `ml-length-sq`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index