---

Step * 1 3 1 of Lemma no_repeats-remove-first


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. ¬(∀j:ℕi + 1. (¬↑(P L[j])))
16. ¬(∀j:ℕj + 1. (¬↑(P L[j])))
17. ¬(i = j ∈ ℤ)
⊢ i = j ∈ ℕ
BY
{ (D (-3)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D (-4)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN (D (-9) THENA (InstConcl [⌜j1⌝]⋅ THEN Auto))
   THEN (D (-8) THENA (InstConcl [⌜j2⌝]⋅ THEN Auto))
   THEN HypSubst' (-2) (-11)
   THEN HypSubst' (-1) (-11)
   THEN InstHyp [⌜i + 1⌝;⌜j + 1⌝] (-16)⋅
   THEN Auto'
   THEN (InstLemma `length-remove-first` [⌜T⌝;⌜L⌝;⌜P⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN With ⌜j1⌝ (D (-2))⋅
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||remove-first(P;L)||
8.  j  <  ||remove-first(P;L)||
9.  remove-first(P;L)[i]  =  remove-first(P;L)[j]
10.  remove-first(P;L)[i]  \msim{}  L[i]  supposing  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j]))
11.  remove-first(P;L)[i]  \msim{}  L[i  +  1]  supposing  \mexists{}j:\mBbbN{}i  +  1.  (\muparrow{}(P  L[j]))
12.  remove-first(P;L)[j]  \msim{}  L[j]  supposing  \mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j]))
13.  remove-first(P;L)[j]  \msim{}  L[j  +  1]  supposing  \mexists{}j:\mBbbN{}j  +  1.  (\muparrow{}(P  L[j]))
14.  ||remove-first(P;L)||  \mleq{}  ||L||
15.  \mneg{}(\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j])))
16.  \mneg{}(\mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j])))
17.  \mneg{}(i  =  j)
\mvdash{}  i  =  j


By

---

Latex:
(D  (-3)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  (-4)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (D  (-9)  THENA  (InstConcl  [\mkleeneopen{}j1\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (D  (-8)  THENA  (InstConcl  [\mkleeneopen{}j2\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  HypSubst'  (-2)  (-11)
  THEN  HypSubst'  (-1)  (-11)
  THEN  InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{};\mkleeneopen{}j  +  1\mkleeneclose{}]  (-16)\mcdot{}
  THEN  Auto'
  THEN  (InstLemma  `length-remove-first`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  With  \mkleeneopen{}j1\mkleeneclose{}  (D  (-2))\mcdot{}
  THEN  Auto')\mcdot{}

---

Home Index