---

Step * 1 2 of Lemma sublist_pair


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)
BY
{ ((D 0 THENA Auto) THEN IntSegCases (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}||L||
4.  j  :  \mBbbN{}||L||
5.  i  <  j
\mvdash{}  \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  THENA  Auto)  THEN  IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index