---

Step * 2 of Lemma finite-function-equipollent-tuple


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)))
BY
{ (RWO "upto_decomp1" 0 THENA Auto) }

1
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 - 1) @ [n - 1]))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  [\%1]  :  0  <  n@i
3.  \mforall{}F:\mBbbN{}n  -  1  {}\mrightarrow{}  Type.  i:\mBbbN{}n  -  1  {}\mrightarrow{}  F[i]  \msim{}  tuple-type(map(\mlambda{}i.F[i];upto(n  -  1)))@i'
4.  F  :  \mBbbN{}n  {}\mrightarrow{}  Type@i'
\mvdash{}  i:\mBbbN{}n  {}\mrightarrow{}  F[i]  \msim{}  tuple-type(map(\mlambda{}i.F[i];upto(n)))


By

---

Latex:
(RWO  "upto\_decomp1"  0  THENA  Auto)

---

Home Index