---

Step * 1 of Lemma sorted-by-no_repeats


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
BY
{ (((Assert ⌜R L[i] L[j]⌝⋅ BY Auto) THEN (HypSubst' -3 -1 THENA Auto)) THEN Assert ⌜¬(R L[j] L[j])⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  (\mneg{}(R  x  x))
4.  L  :  T  List
5.  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    (R  L[j]  L[i])
6.  i  :  \mBbbN{}
7.  j  :  \mBbbN{}
8.  i  <  ||L||
9.  j  <  ||L||
10.  \mneg{}(i  =  j)
11.  L[i]  =  L[j]
12.  i  <  j
\mvdash{}  False


By

---

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

---

Home Index