---

Step * of Lemma no_repeats_l_index

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[i:ℕ||L||].  index(L;L[i]) ~ i supposing no_repeats(T;L)
BY
{ ((UnivCD THENA Auto)
   THEN (Assert index(L;L[i]) = i ∈ ℤ BY
               (Unfold `l_index` 0 THEN BLemma `no_repeats_mu_index` THEN Auto))
   THEN (HypSubst' (-1) 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[i:\mBbbN{}||L||].
    index(L;L[i])  \msim{}  i  supposing  no\_repeats(T;L)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  index(L;L[i])  =  i  BY
                          (Unfold  `l\_index`  0  THEN  BLemma  `no\_repeats\_mu\_index`  THEN  Auto))
  THEN  (HypSubst'  (-1)  0)
  THEN  Auto)

---

Home Index