---

Step * 1 of Lemma sublist_nil


1. T : Type
2. L : T List
3. L ⊆ []
⊢ L = [] ∈ (T List)
BY
{ (BackThruLemma `length_zero`
   THEN Auto
   THEN (FwdThruLemma `length_sublist` [(-1)])
   THEN Auto
   THEN (Reduce (-1))
   THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  L  \msubseteq{}  []
\mvdash{}  L  =  []


By

---

Latex:
(BackThruLemma  `length\_zero`
  THEN  Auto
  THEN  (FwdThruLemma  `length\_sublist`  [(-1)])
  THEN  Auto
  THEN  (Reduce  (-1))
  THEN  Auto')

---

Home Index