---

Step * of Lemma len_wf

∀[as:Top List]. (len(as) ∈ ℕ)
BY
{ (InductionOnList THEN Unfold `len` 0 THEN Reduce 0 THEN Try (Fold `len` 0) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[as:Top  List].  (len(as)  \mmember{}  \mBbbN{})


By

---

Latex:
(InductionOnList  THEN  Unfold  `len`  0  THEN  Reduce  0  THEN  Try  (Fold  `len`  0)  THEN  Auto')

---

Home Index