---

Step * of Lemma enum-fin-seq_wf

∀[m:ℕ]. (enum-fin-seq(m) ∈ ℕ ⟶ 𝔹 List(2^m))
BY
{ ((UnivCD THENA Auto) THEN (MemTypeCD THENA Auto)) }

1
1. m : ℕ
⊢ enum-fin-seq(m) ∈ (ℕ ⟶ 𝔹) List

2
.....set predicate..... 
1. m : ℕ
⊢ ||enum-fin-seq(m)|| = 2^m ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}].  (enum-fin-seq(m)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}  List(2\^{}m))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (MemTypeCD  THENA  Auto))

---

Home Index