---

Step * of Lemma member_iff_sublist

∀[T:Type]. ∀x:T. ∀L:T List.  ((x ∈ L) ⇐⇒ [x] ⊆ L)
BY
{ (Unfolds ``l_member sublist`` 0
   THEN Auto'
   THEN Try ((Unfold `label` 0 THEN Reduce 0 THEN Auto'))
   THEN All Reduce
   THEN ExRepD) }

1
1. [T] : Type
2. x : T
3. L : T List
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
⊢ ∃f:ℕ1 ⟶ ℕ||L||. (increasing(f;1) ∧ (∀j:ℕ1. ([x][j] = L[f j] ∈ T)))

2
1. [T] : Type
2. x : T
3. L : T List
4. f : ℕ1 ⟶ ℕ||L||
5. increasing(f;1)
6. ∀j:ℕ1. ([x][j] = L[f j] ∈ T)
⊢ ∃i:ℕ. (i < ||L|| c∧ (x = L[i] ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:T  List.    ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  [x]  \msubseteq{}  L)


By

---

Latex:
(Unfolds  ``l\_member  sublist``  0
  THEN  Auto'
  THEN  Try  ((Unfold  `label`  0  THEN  Reduce  0  THEN  Auto'))
  THEN  All  Reduce
  THEN  ExRepD)

---

Home Index