---

Step * of Lemma non_nil_length

∀[T:Type]. ∀[L:T List].  0 < ||L|| supposing ¬(L = [] ∈ (T List))
BY
{ ((Auto THEN ListInd (-2)) THEN Reduce 0 THEN Auto THEN D (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    0  <  ||L||  supposing  \mneg{}(L  =  [])


By

---

Latex:
((Auto  THEN  ListInd  (-2))  THEN  Reduce  0  THEN  Auto  THEN  D  (-1)  THEN  Auto)

---

Home Index