---

Step * of Lemma no_repeats-remove-first

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  no_repeats(T;remove-first(P;L)) supposing no_repeats(T;L)
BY
{ ((UnivCD THENA Auto)
   THEN All (Unfold `no_repeats`)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D (-2)
   THEN (InstLemma `select-remove-first` [⌜T⌝;⌜L⌝;⌜P⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜i⌝] (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜j⌝] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN Auto
   THEN (InstLemma `length-remove-first-le` [⌜T⌝;⌜L⌝;⌜P⌝]⋅ THENA Auto)
   THEN (Assert ⌜Dec(∀j:ℕi + 1. (¬↑(P L[j])))⌝⋅ THENA Auto)
   THEN (Assert ⌜Dec(∀j:ℕj + 1. (¬↑(P L[j])))⌝⋅ THENA Auto)) }

1
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)}  ⟶ 𝔹
4. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. i : ℕ
6. j : ℕ
7. i < ||remove-first(P;L)||
8. j < ||remove-first(P;L)||
9. remove-first(P;L)[i] = remove-first(P;L)[j] ∈ T
10. remove-first(P;L)[i] ~ L[i] supposing ∀j:ℕi + 1. (¬↑(P L[j]))
11. remove-first(P;L)[i] ~ L[i + 1] supposing ∃j:ℕi + 1. (↑(P L[j]))
12. remove-first(P;L)[j] ~ L[j] supposing ∀j:ℕj + 1. (¬↑(P L[j]))
13. remove-first(P;L)[j] ~ L[j + 1] supposing ∃j:ℕj + 1. (↑(P L[j]))
14. ||remove-first(P;L)|| ≤ ||L||
15. Dec(∀j:ℕi + 1. (¬↑(P L[j])))
16. Dec(∀j:ℕj + 1. (¬↑(P L[j])))
⊢ i = j ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].
    no\_repeats(T;remove-first(P;L))  supposing  no\_repeats(T;L)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All  (Unfold  `no\_repeats`)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  (-2)
  THEN  (InstLemma  `select-remove-first`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  Auto
  THEN  (InstLemma  `length-remove-first-le`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}Dec(\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j])))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}Dec(\mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j])))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index