---

Step * of Lemma length-zero-implies-sq-nil

∀l:Top List. l ~ [] supposing ||l|| = 0 ∈ ℤ
BY
{ (Auto THEN D 1 THEN AllReduce THEN Auto') }

---

Latex:

---

Latex:
\mforall{}l:Top  List.  l  \msim{}  []  supposing  ||l||  =  0


By

---

Latex:
(Auto  THEN  D  1  THEN  AllReduce  THEN  Auto')

---

Home Index