---

Step * 1 of Lemma lastn-0

.....truecase..... 
1. L : Top List
2. n : ℤ
3. n ≤ 0
4. ||L|| ≤ n
⊢ L ~ []
BY
{ (DVar `L' THEN All Reduce⋅ THEN Auto') }

---

Latex:

---

Latex:
.....truecase..... 
1.  L  :  Top  List
2.  n  :  \mBbbZ{}
3.  n  \mleq{}  0
4.  ||L||  \mleq{}  n
\mvdash{}  L  \msim{}  []


By

---

Latex:
(DVar  `L'  THEN  All  Reduce\mcdot{}  THEN  Auto')

---

Home Index