---

Step * of Lemma sorted-by-strict-no_repeats

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L:T List].  (no_repeats(T;L)) supposing (sorted-by(R;L) and (∀a:T. (¬(R a a))))
BY
{ (Auto THEN D 0 THEN Auto THEN ParallelLast) }

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
⊢ i = j ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[L:T  List].
    (no\_repeats(T;L))  supposing  (sorted-by(R;L)  and  (\mforall{}a:T.  (\mneg{}(R  a  a))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  ParallelLast)

---

Home Index