---

Step * 1 of Lemma decidable__no_repeats


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

1
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||)

2
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||))

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (ParallelLast)

---

Home Index