---

Step * 1 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]
7. x : ℕn
⊢ (a1 x) = (a2 x) ∈ F[x]
BY
{ (Decide x = (n - 1) ∈ ℤ THENA 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
8. x = (n - 1) ∈ ℤ
⊢ (a1 x) = (a2 x) ∈ F[x]

2
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
8. ¬(x = (n - 1) ∈ ℤ)
⊢ (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))
7.  x  :  \mBbbN{}n
\mvdash{}  (a1  x)  =  (a2  x)


By

---

Latex:
(Decide  x  =  (n  -  1)  THENA  Auto)

---

Home Index