---

Step * 1 of Lemma equipollent-list


1. [T] : Type
2. n : ℕ
⊢ {as:T List| ||as|| = n ∈ ℤ}  ~ ℕn ⟶ T
BY
{ (With ⌜λL,i. L[i]⌝ (D 0)⋅ THEN Auto)⋅ }

1
1. [T] : Type
2. n : ℕ
⊢ Bij({as:T List| ||as|| = n ∈ ℤ} ;ℕn ⟶ T;λL,i. L[i])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}
\mvdash{}  \{as:T  List|  ||as||  =  n\}    \msim{}  \mBbbN{}n  {}\mrightarrow{}  T


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}L,i.  L[i]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index