---

Step * 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, a1 (n - 1)> = <a2, a2 (n - 1)> ∈ (i:ℕn - 1 ⟶ F[i] × F[n - 1])
⊢ a1 = a2 ∈ (i:ℕn ⟶ F[i])
BY
{ AutoSimpHyp Auto (-1) }

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]
⊢ a1 = a2 ∈ (i:ℕn ⟶ F[i])

---

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,  a1  (n  -  1)>  =  <a2,  a2  (n  -  1)>
\mvdash{}  a1  =  a2


By

---

Latex:
AutoSimpHyp  Auto  (-1)

---

Home Index