---

Step * of Lemma non_null_iff_length

∀[L:Top List]. uiff(¬↑null(L);0 < ||L||)
BY
{ ((UnivCD THENA Auto) THEN DVar `L' THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  uiff(\mneg{}\muparrow{}null(L);0  <  ||L||)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  DVar  `L'  THEN  Reduce  0  THEN  Auto')

---

Home Index