---

Step * of Lemma no_repeats_mu_index

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[i:ℕ||L||].  mu(λi@0.(eq L[i] L[i@0])) = i ∈ ℤ supposing no_repeats(T;L)
BY
{ (Auto
   THEN (Using [`b',⌜||L||⌝] (BLemma `mu-bound-unique`))⋅
   THEN Reduce 0
   THEN Auto
   THEN All (RW assert_pushdownC)
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||L||
5. no_repeats(T;L)
6. L[i] = L[i] ∈ T
7. y : ℕ||L||@i
8. L[i] = L[y] ∈ T
⊢ y = i ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[i:\mBbbN{}||L||].
    mu(\mlambda{}i@0.(eq  L[i]  L[i@0]))  =  i  supposing  no\_repeats(T;L)


By

---

Latex:
(Auto
  THEN  (Using  [`b',\mkleeneopen{}||L||\mkleeneclose{}]  (BLemma  `mu-bound-unique`))\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  All  (RW  assert\_pushdownC)
  THEN  Auto)

---

Home Index