---

Step * 1 of Lemma decidable__exists_length

.....assertion..... 
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
⊢ {as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n
BY
{ (BLemma `equipollent-list` THEN Auto)⋅ }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}L:T  List.  Dec(P[L])
4.  k  :  \mBbbN{}
5.  T  \msim{}  \mBbbN{}k
6.  n  :  \mBbbN{}
\mvdash{}  \{as:T  List|  ||as||  =  n\}    \msim{}  \mBbbN{}k\^{}n


By

---

Latex:
(BLemma  `equipollent-list`  THEN  Auto)\mcdot{}

---

Home Index