---

Step * of Lemma finite-function-equipollent-tuple

∀n:ℕ. ∀F:ℕn ⟶ Type.  i:ℕn ⟶ F[i] ~ tuple-type(map(λi.F[i];upto(n)))
BY
{ (InductionOnNat THEN Auto) }

1
1. F : ℕ0 ⟶ Type@i'
⊢ i:ℕ0 ⟶ F[i] ~ tuple-type(map(λi.F[i];upto(0)))

2
1. n : ℤ@i
2. [%1] : 0 < n@i
3. ∀F:ℕn - 1 ⟶ Type. i:ℕn - 1 ⟶ F[i] ~ tuple-type(map(λi.F[i];upto(n - 1)))@i'
4. F : ℕn ⟶ Type@i'
⊢ i:ℕn ⟶ F[i] ~ tuple-type(map(λi.F[i];upto(n)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}F:\mBbbN{}n  {}\mrightarrow{}  Type.    i:\mBbbN{}n  {}\mrightarrow{}  F[i]  \msim{}  tuple-type(map(\mlambda{}i.F[i];upto(n)))


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index