---

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


1. [T] : Type
2. u : T@i
3. v : T List@i
4. ∀l1:T List. (l1 ⊆ v ⇐⇒ sublist-rec(T;l1;v))@i
5. l1 : T List@i
6. sublist-rec(T;l1;[u / v])@i
⊢ l1 ⊆ [u / v]
BY
{ (DVar `l1'
   THEN RecUnfold `sublist-rec` (-1)
   THEN Reduce (-1)
   THEN Try (Complete ((BLemma `nil_sublist` THEN Auto)))
   THEN (RWO "cons_sublist_cons" 0 THENA Auto)
   THEN D (-1)
   THEN RepD
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T@i
3.  v  :  T  List@i
4.  \mforall{}l1:T  List.  (l1  \msubseteq{}  v  \mLeftarrow{}{}\mRightarrow{}  sublist-rec(T;l1;v))@i
5.  l1  :  T  List@i
6.  sublist-rec(T;l1;[u  /  v])@i
\mvdash{}  l1  \msubseteq{}  [u  /  v]


By

---

Latex:
(DVar  `l1'
  THEN  RecUnfold  `sublist-rec`  (-1)
  THEN  Reduce  (-1)
  THEN  Try  (Complete  ((BLemma  `nil\_sublist`  THEN  Auto)))
  THEN  (RWO  "cons\_sublist\_cons"  0  THENA  Auto)
  THEN  D  (-1)
  THEN  RepD
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index