---

Step * of Lemma finite-function-equipollent

∀n:ℕ+. ∀[F:ℕn ⟶ Type]. i:ℕn ⟶ F[i] ~ i:ℕn - 1 ⟶ F[i] × F[n - 1]
BY
{ Auto }

1
1. n : ℕ+
2. [F] : ℕn ⟶ Type
⊢ i:ℕn ⟶ F[i] ~ i:ℕn - 1 ⟶ F[i] × F[n - 1]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}[F:\mBbbN{}n  {}\mrightarrow{}  Type].  i:\mBbbN{}n  {}\mrightarrow{}  F[i]  \msim{}  i:\mBbbN{}n  -  1  {}\mrightarrow{}  F[i]  \mtimes{}  F[n  -  1]


By

---

Latex:
Auto

---

Home Index