---

Step * 1 of Lemma sqequal-null


1. T : Type
2. l : T List
3. ↑null(l)
⊢ l = [] ∈ (T List)
BY
{ (RW  assert_pushdownC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \muparrow{}null(l)
\mvdash{}  l  =  []


By

---

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

---

Home Index