---

Step * 1 1 1 of Lemma no_repeats_iff

.....antecedent..... 
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
⊢ ¬((f 0) = (f 1) ∈ ℕ)
BY
{ ((Unfold `increasing` (-4) THEN InstHyp [0] (-4)) THEN Auto) }

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. ∀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) ∈ ℕ)

---

Latex:

---

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


By

---

Latex:
((Unfold  `increasing`  (-4)  THEN  InstHyp  [0]  (-4))  THEN  Auto)

---

Home Index