---

Step * of Lemma sorted-by-no_repeats

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀[L:T List]. no_repeats(T;L) supposing sorted-by(R;L) supposing ∀x:T. (¬(R x x))
BY
{ (Auto THEN UnfoldTopAb (-1) THEN (D 0 THEN Auto) THEN (D 0 THENA Auto) THEN (Decide ⌜i < j⌝⋅ THENA Auto)) }

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

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

---

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)  supposing  \mforall{}x:T.  (\mneg{}(R  x  x))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  (D  0  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}i  <  j\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index