---

Step * 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. 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)
BY
{ (AllHyps (InstHyp [f 0;f 1]) THEN Auto) }

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

---

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.  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{}(x  =  y)


By

---

Latex:
(AllHyps  (InstHyp  [f  0;f  1])  THEN  Auto)

---

Home Index