---

Step * 1 1 1 1 of Lemma finite-function-equipollent


1. n : ℕ+
2. F : ℕn ⟶ Type
3. a1 : i:ℕn ⟶ F[i]
4. a2 : i:ℕn ⟶ F[i]
5. a1 = a2 ∈ (i:ℕn - 1 ⟶ F[i])
6. (a1 (n - 1)) = (a2 (n - 1)) ∈ F[n - 1]
⊢ a1 = a2 ∈ (i:ℕn ⟶ F[i])
BY
{ (Ext THEN Auto) }

1
1. n : ℕ+
2. F : ℕn ⟶ Type
3. a1 : i:ℕn ⟶ F[i]
4. a2 : i:ℕn ⟶ F[i]
5. a1 = a2 ∈ (i:ℕn - 1 ⟶ F[i])
6. (a1 (n - 1)) = (a2 (n - 1)) ∈ F[n - 1]
7. x : ℕn
⊢ (a1 x) = (a2 x) ∈ F[x]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  F  :  \mBbbN{}n  {}\mrightarrow{}  Type
3.  a1  :  i:\mBbbN{}n  {}\mrightarrow{}  F[i]
4.  a2  :  i:\mBbbN{}n  {}\mrightarrow{}  F[i]
5.  a1  =  a2
6.  (a1  (n  -  1))  =  (a2  (n  -  1))
\mvdash{}  a1  =  a2


By

---

Latex:
(Ext  THEN  Auto)

---

Home Index