---

Step * 1 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
11. i < j
⊢ i = j ∈ ℕ
BY
{ ((Assert R L[i] L[j] BY Auto) THEN (HypSubst' -3 -1 THENA Auto) THEN InstHyp [⌜L[j]⌝] 4⋅ THEN Auto) }

---

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]
11.  i  <  j
\mvdash{}  i  =  j


By

---

Latex:
((Assert  R  L[i]  L[j]  BY  Auto)  THEN  (HypSubst'  -3  -1  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}L[j]\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index