---

Step * of Lemma even-int-list_wf

∀[L:ℤ List]. (even-int-list(L) ∈ 𝔹)
BY
{ InductionOnLength }

1
1. n : ℕ
2. L : ℤ List
3. ∀L1:ℤ List. (||L1|| < ||L|| ⇒ (even-int-list(L1) ∈ 𝔹))
⊢ even-int-list(L) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  (even-int-list(L)  \mmember{}  \mBbbB{})


By

---

Latex:
InductionOnLength

---

Home Index