---

Step * 1 of Lemma sublist_pair


1. [T] : Type
2. L : T List
3. i : ℕ||L||
4. j : ℕ||L||
5. i < j
⊢ increasing(λn.if (n =z 0) then i else j fi ;2)
∧ (∀j@0:ℕ2. ([L[i]; L[j]][j@0] = L[(λn.if (n =z 0) then i else j fi ) j@0] ∈ T))
BY
{ D 0 }

1
1. [T] : Type
2. L : T List
3. i : ℕ||L||
4. j : ℕ||L||
5. i < j
⊢ increasing(λn.if (n =z 0) then i else j fi ;2)

2
1. [T] : Type
2. L : T List
3. i : ℕ||L||
4. j : ℕ||L||
5. i < j
⊢ ∀j@0:ℕ2. ([L[i]; L[j]][j@0] = L[(λn.if (n =z 0) then i else j fi ) j@0] ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}||L||
4.  j  :  \mBbbN{}||L||
5.  i  <  j
\mvdash{}  increasing(\mlambda{}n.if  (n  =\msubz{}  0)  then  i  else  j  fi  ;2)
\mwedge{}  (\mforall{}j@0:\mBbbN{}2.  ([L[i];  L[j]][j@0]  =  L[(\mlambda{}n.if  (n  =\msubz{}  0)  then  i  else  j  fi  )  j@0]))


By

---

Latex:
D  0

---

Home Index