---

Step * 1 of Lemma member_iff_sublist


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)))
BY
{ (InstConcl [λx.i]⋅ THEN Auto THEN Try ((Unfold `label` 0 THEN Reduce 0 THEN Auto))) }

1
1. [T] : Type
2. x : T
3. L : T List
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
⊢ increasing(λx.i;1)

2
1. T : Type
2. x : T
3. L : T List
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
7. increasing(λx.i;1)
8. j : ℕ1
⊢ [x][j] = L[(λx.i) j] ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  L  :  T  List
4.  i  :  \mBbbN{}
5.  i  <  ||L||
6.  x  =  L[i]
\mvdash{}  \mexists{}f:\mBbbN{}1  {}\mrightarrow{}  \mBbbN{}||L||.  (increasing(f;1)  \mwedge{}  (\mforall{}j:\mBbbN{}1.  ([x][j]  =  L[f  j])))


By

---

Latex:
(InstConcl  [\mlambda{}x.i]\mcdot{}  THEN  Auto  THEN  Try  ((Unfold  `label`  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index