---

Step * 1 1 1 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||
7. ∀i:ℕ||[x; y]|| - 1. f i < f (i + 1)
8. ∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)
9. x = l[f 0] ∈ T
10. y = l[f 1] ∈ T
11. f 0 < f (0 + 1)
⊢ ¬((f 0) = (f 1) ∈ ℕ)
BY
{ (All Reduce THEN Auto) }

---

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.  f  :  \mBbbN{}||[x;  y]||  {}\mrightarrow{}  \mBbbN{}||l||
7.  \mforall{}i:\mBbbN{}||[x;  y]||  -  1.  f  i  <  f  (i  +  1)
8.  \mforall{}j:\mBbbN{}||[x;  y]||.  ([x;  y][j]  =  l[f  j])
9.  x  =  l[f  0]
10.  y  =  l[f  1]
11.  f  0  <  f  (0  +  1)
\mvdash{}  \mneg{}((f  0)  =  (f  1))


By

---

Latex:
(All  Reduce  THEN  Auto)

---

Home Index