---

Step * of Lemma decidable__no_repeats

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀L:T List. Dec(no_repeats(T;L))))
BY
{ (Auto
   THEN Unfold `no_repeats` 0
   THEN (Assert ⌜Dec(∀i,j:ℕ||L||.  ((¬(i = j ∈ ℕ)) ⇒ (¬(L[i] = L[j] ∈ T))))⌝⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L:T  List.  Dec(no\_repeats(T;L))))


By

---

Latex:
(Auto
  THEN  Unfold  `no\_repeats`  0
  THEN  (Assert  \mkleeneopen{}Dec(\mforall{}i,j:\mBbbN{}||L||.    ((\mneg{}(i  =  j))  {}\mRightarrow{}  (\mneg{}(L[i]  =  L[j]))))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index