---

Step * 2 of Lemma sublist-rec-iff-sublist


1. T : Type
2. l1 : T List@i
3. sublist-rec(T;l1;[])@i
⊢ l1 = [] ∈ (T List)
BY
{ (DVar `l1' THEN RecUnfold `sublist-rec` (-1) THEN Reduce (-1) THEN Auto THEN BLemma `sublist_nil` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l1  :  T  List@i
3.  sublist-rec(T;l1;[])@i
\mvdash{}  l1  =  []


By

---

Latex:
(DVar  `l1'
  THEN  RecUnfold  `sublist-rec`  (-1)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  BLemma  `sublist\_nil`
  THEN  Auto)

---

Home Index