---

Step * 1 of Lemma sorted-by-strict-no_repeats


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. L : T List
4. ∀a:T. (¬(R a a))
5. sorted-by(R;L)
6. i : ℕ
7. j : ℕ
8. i < ||L||
9. j < ||L||
10. L[i] = L[j] ∈ T
⊢ i = j ∈ ℕ
BY
{ (Decide i < j THENA Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. L : T List
4. ∀a:T. (¬(R a a))
5. sorted-by(R;L)
6. i : ℕ
7. j : ℕ
8. i < ||L||
9. j < ||L||
10. L[i] = L[j] ∈ T
11. i < j
⊢ i = j ∈ ℕ

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. L : T List
4. ∀a:T. (¬(R a a))
5. sorted-by(R;L)
6. i : ℕ
7. j : ℕ
8. i < ||L||
9. j < ||L||
10. L[i] = L[j] ∈ T
11. ¬i < j
⊢ i = j ∈ ℕ

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  L  :  T  List
4.  \mforall{}a:T.  (\mneg{}(R  a  a))
5.  sorted-by(R;L)
6.  i  :  \mBbbN{}
7.  j  :  \mBbbN{}
8.  i  <  ||L||
9.  j  <  ||L||
10.  L[i]  =  L[j]
\mvdash{}  i  =  j


By

---

Latex:
(Decide  i  <  j  THENA  Auto)

---

Home Index