---

Step * 1 1 of Lemma equipollent-list


1. [T] : Type
2. n : ℕ
⊢ Bij({as:T List| ||as|| = n ∈ ℤ} ;ℕn ⟶ T;λL,i. L[i])
BY
{ (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto THEN All DSet THEN Auto') }

1
1. T : Type
2. n : ℕ
3. a1 : T List
4. ||a1|| = n ∈ ℤ
5. a2 : T List
6. ||a2|| = n ∈ ℤ
7. (λi.a1[i]) = (λi.a2[i]) ∈ (ℕn ⟶ T)
⊢ a1 = a2 ∈ {as:T List| ||as|| = n ∈ ℤ} 

2
1. [T] : Type
2. n : ℕ
3. b : ℕn ⟶ T
⊢ ∃a:{as:T List| ||as|| = n ∈ ℤ} . ((λi.a[i]) = b ∈ (ℕn ⟶ T))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}
\mvdash{}  Bij(\{as:T  List|  ||as||  =  n\}  ;\mBbbN{}n  {}\mrightarrow{}  T;\mlambda{}L,i.  L[i])


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto  THEN  All  DSet  THEN  Auto')

---

Home Index