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