---

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


1. [T] : Type
2. l1 : T List@i
3. l1 ⊆ []@i
⊢ sublist-rec(T;l1;[])
BY
{ (DVar `l1'
   THEN Try (Complete ((RWO "cons_sublist_nil" (-1) THEN Auto)))
   THEN RecUnfold `sublist-rec` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(DVar  `l1'
  THEN  Try  (Complete  ((RWO  "cons\_sublist\_nil"  (-1)  THEN  Auto)))
  THEN  RecUnfold  `sublist-rec`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index