---

Step * 3 of Lemma strict-sorted


1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]
⊢ no_repeats(T;as)
BY
{ xxx((Unfold `no_repeats` 0 THEN Auto THEN Decide ⌜i < j⌝⋅) THENA Auto)xxx }

1
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]
5. i : ℕ
6. j : ℕ
7. i < ||as||
8. j < ||as||
9. ¬(i = j ∈ ℕ)
10. i < j
⊢ ¬(as[i] = as[j] ∈ T)

2
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]
5. i : ℕ
6. j : ℕ
7. i < ||as||
8. j < ||as||
9. ¬(i = j ∈ ℕ)
10. ¬i < j
⊢ ¬(as[i] = as[j] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  \mBbbZ{}
3.  as  :  T  List
4.  \mforall{}[i:\mBbbN{}||as||].  \mforall{}[j:\mBbbN{}i].    as[j]  <  as[i]
\mvdash{}  no\_repeats(T;as)


By

---

Latex:
xxx((Unfold  `no\_repeats`  0  THEN  Auto  THEN  Decide  \mkleeneopen{}i  <  j\mkleeneclose{}\mcdot{})  THENA  Auto)xxx

---

Home Index