---

Step * of Lemma select-indices-aux_wf

∀[A:Type]. ∀[f:A ─→ 𝔹]. ∀[L:A List].  (select-indices-aux(f;L) ∈ ℕ ─→ (ℕ List))
BY
{ InductionOnList }

1
1. A : Type
2. f : A ─→ 𝔹
⊢ select-indices-aux(f;[]) ∈ ℕ ─→ (ℕ List)

2
1. A : Type
2. f : A ─→ 𝔹
3. u : A
4. v : A List
5. select-indices-aux(f;v) ∈ ℕ ─→ (ℕ List)
⊢ select-indices-aux(f;[u / v]) ∈ ℕ ─→ (ℕ List)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].    (select-indices-aux(f;L)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  List))


By

---

Latex:
InductionOnList

---

Home Index