---

Step * of Lemma no_repeats_cons

∀[T:Type]. ∀[l:T List]. ∀[x:T].  uiff(no_repeats(T;[x / l]);no_repeats(T;l) ∧ (¬(x ∈ l)))
BY
{ ((Unfold `no_repeats` 0 THEN Reduce 0) THEN Auto') }

1
1. T : Type
2. l : T List
3. x : T
4. ∀[i,j:ℕ].  (¬([x / l][i] = [x / l][j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| + 1 and i < ||l|| + 1)
5. i : ℕ
6. j : ℕ
7. i < ||l||
8. j < ||l||
9. ¬(i = j ∈ ℕ)
⊢ ¬(l[i] = l[j] ∈ T)

2
1. T : Type
2. l : T List
3. x : T
4. ∀[i,j:ℕ].  (¬([x / l][i] = [x / l][j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| + 1 and i < ||l|| + 1)
⊢ ¬(x ∈ l)

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[x:T].    uiff(no\_repeats(T;[x  /  l]);no\_repeats(T;l)  \mwedge{}  (\mneg{}(x  \mmember{}  l)))


By

---

Latex:
((Unfold  `no\_repeats`  0  THEN  Reduce  0)  THEN  Auto')

---

Home Index