---

Step * of Lemma length-zero-implies-nil

∀l:Base. l ~ [] supposing ||l|| = 0 ∈ ℤ
BY
{ (Auto THEN (Assert (||l||)↓ BY Auto)) }

1
1. l : Base@i
2. ||l|| = 0 ∈ ℤ
3. (||l||)↓
⊢ l = [] ∈ Base

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Assert  (||l||)\mdownarrow{}  BY  Auto))

---

Home Index