---

Step * of Lemma sublist-rec-iff-sublist

∀[T:Type]. ∀l1,l2:T List.  (l1 ⊆ l2 ⇐⇒ sublist-rec(T;l1;l2))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN MoveToConcl (-2) THEN ListInd (-1) THEN Auto) }

1
1. [T] : Type
2. l1 : T List@i
3. l1 ⊆ []@i
⊢ sublist-rec(T;l1;[])

2
1. T : Type
2. l1 : T List@i
3. sublist-rec(T;l1;[])@i
⊢ l1 = [] ∈ (T List)

3
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])

4
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]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2:T  List.    (l1  \msubseteq{}  l2  \mLeftarrow{}{}\mRightarrow{}  sublist-rec(T;l1;l2))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  MoveToConcl  (-2)  THEN  ListInd  (-1)  THEN  Auto)

---

Home Index