---

Step * 1 1 of Lemma last-lemma-sq

.....assertion..... 
1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ ||L|| > 0
BY
{ ((RW assert_pushdownC (-1)) THEN Auto THEN Easy) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  L  :  T  List
3.  \mneg{}\muparrow{}null(L)
\mvdash{}  ||L||  >  0


By

---

Latex:
((RW  assert\_pushdownC  (-1))  THEN  Auto  THEN  Easy)

---

Home Index