---

Step * 3 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. l1 ⊆ [u / v]@i
⊢ sublist-rec(T;l1;[u / v])
BY
{ (DVar `l1'
   THEN Try (Complete ((RecUnfold `sublist-rec` 0 THEN Reduce 0 THEN Auto)))
   THEN (RWO "cons_sublist_cons" (-1) THENA Auto)
   THEN D (-1)
   THEN RepD
   THEN RecUnfold `sublist-rec` 0
   THEN Reduce 0
   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.  l1  \msubseteq{}  [u  /  v]@i
\mvdash{}  sublist-rec(T;l1;[u  /  v])


By

---

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

---

Home Index