---

Step * of Lemma finite-fixed-length

∀T:Type. ∀n:ℕ.  (finite(T) ⇒ finite({l:T List| ||l|| = n ∈ ℤ} ))
BY
{ (Auto THEN D -1 THEN (InstLemma `equipollent-list` [⌜T⌝;⌜n1⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. T : Type
2. n : ℕ
3. n1 : ℕ
4. T ~ ℕn1
5. {as:T List| ||as|| = n ∈ ℤ}  ~ ℕn1^n
⊢ finite({l:T List| ||l|| = n ∈ ℤ} )

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}n:\mBbbN{}.    (finite(T)  {}\mRightarrow{}  finite(\{l:T  List|  ||l||  =  n\}  ))


By

---

Latex:
(Auto  THEN  D  -1  THEN  (InstLemma  `equipollent-list`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index