---

Step * 3 2 of Lemma strict-sorted


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)
BY
{ xxx((InstHyp [⌜i⌝; ⌜j⌝] 4)⋅ THEN Auto' THEN D 0 THEN Auto THEN (HypSubst' (-1) (-2)) THEN Auto)xxx }

---

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]
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||as||
8.  j  <  ||as||
9.  \mneg{}(i  =  j)
10.  \mneg{}i  <  j
\mvdash{}  \mneg{}(as[i]  =  as[j])


By

---

Latex:
xxx((InstHyp  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}j\mkleeneclose{}]  4)\mcdot{}  THEN  Auto'  THEN  D  0  THEN  Auto  THEN  (HypSubst'  (-1)  (-2))  THEN  Auto)xxx

---

Home Index