---

Step * 2 1 2 of Lemma no_repeats_iff


1. T : Type
2. l : T List
3. ∀[x,y:T].  ¬(x = y ∈ T) supposing ∃f:ℕ2 ⟶ ℕ||l||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. i < j
10. increasing(λx.if (x =z 0) then i else j fi ;2)
11. j1 : ℕ2
⊢ [l[i]; l[j]][j1] = l[if (j1 =z 0) then i else j fi ] ∈ T
BY
{ (IntSegCases (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  \mexists{}f:\mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||l||.  (increasing(f;2)  \mwedge{}  (\mforall{}j:\mBbbN{}2.  ([x;  y][j]  =  l[f  j])))
4.  i  :  \mBbbN{}
5.  j  :  \mBbbN{}
6.  i  <  ||l||
7.  j  <  ||l||
8.  \mneg{}(i  =  j)
9.  i  <  j
10.  increasing(\mlambda{}x.if  (x  =\msubz{}  0)  then  i  else  j  fi  ;2)
11.  j1  :  \mBbbN{}2
\mvdash{}  [l[i];  l[j]][j1]  =  l[if  (j1  =\msubz{}  0)  then  i  else  j  fi  ]


By

---

Latex:
(IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index