---

Step * 1 1 of Lemma decidable__no_repeats


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. L : T List
4. ∀i,j:ℕ||L||.  ((¬(i = j ∈ ℕ)) ⇒ (¬(L[i] = L[j] ∈ T)))
⊢ ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  L  :  T  List
4.  \mforall{}i,j:\mBbbN{}||L||.    ((\mneg{}(i  =  j))  {}\mRightarrow{}  (\mneg{}(L[i]  =  L[j])))
\mvdash{}  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)


By

---

Latex:
Auto

---

Home Index