---

Step * of Lemma no_repeats_iff

No Annotations
∀[T:Type]. ∀[l:T List].  uiff(no_repeats(T;l);∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ l)
BY
{ ((Unfolds ``no_repeats l_before`` 0 THEN Unfold `sublist` 0) 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||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
⊢ ¬(x = y ∈ T)

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[l:T  List].    uiff(no\_repeats(T;l);\mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  x  before  y  \mmember{}  l)


By

---

Latex:
((Unfolds  ``no\_repeats  l\_before``  0  THEN  Unfold  `sublist`  0)  THEN  Auto')

---

Home Index