---

Step * 1 2 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
{ (ParallelLast THEN Auto THEN BHyp (-4)  THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(ParallelLast  THEN  Auto  THEN  BHyp  (-4)    THEN  Auto)

---

Home Index