---

Step * 1 of Lemma no_repeats_iff


1. T : Type
2. l : T List
3. ∀[i,j:ℕ].  (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
4. x : T
5. y : T
6. ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
⊢ ¬(x = y ∈ T)
BY
{ ((((((ExRepD THEN InstHyp [0] (-1)) THENA Auto) THEN Reduce (-1)) THEN InstHyp [1] (-2)) THENA Auto)
   THEN Reduce (-1)
   ) }

1
1. T : Type
2. l : T List
3. ∀[i,j:ℕ].  (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
4. x : T
5. y : T
6. f : ℕ||[x; y]|| ⟶ ℕ||l||
7. increasing(f;||[x; y]||)
8. ∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)
9. x = l[f 0] ∈ T
10. y = l[f 1] ∈ T
⊢ ¬(x = y ∈ T)

---

Latex:

---

Latex:

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


By

---

Latex:
((((((ExRepD  THEN  InstHyp  [0]  (-1))  THENA  Auto)  THEN  Reduce  (-1))  THEN  InstHyp  [1]  (-2))  THENA  Auto)
  THEN  Reduce  (-1)
  )

---

Home Index