---

Step * of Lemma null-length-zero

∀[L:Top List]. null(L) = (||L|| =z 0)
BY
{ ((UnivCD THENA Auto) THEN DVar `L' THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  null(L)  =  (||L||  =\msubz{}  0)


By

---

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

---

Home Index