---

Step * of Lemma list-if-has-value-length2

∀l:Base. l ∈ Base List supposing (||l||)↓
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `length` -1
   THEN FLemma `list-if-has-value-list_ind` [-1]
   THEN Auto
   THEN ProveStrict) }

---

Latex:

---

Latex:
\mforall{}l:Base.  l  \mmember{}  Base  List  supposing  (||l||)\mdownarrow{}


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `length`  -1
  THEN  FLemma  `list-if-has-value-list\_ind`  [-1]
  THEN  Auto
  THEN  ProveStrict)

---

Home Index