---

Step * 2 1 1 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 - 1)) @ [F[n - 1]])
BY
{ (RWO "tuple-type-append-equipollent<" 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))) × tuple-type([F[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  -  1))  @  [F[n  -  1]])


By

---

Latex:
(RWO  "tuple-type-append-equipollent<"  0  THENA  Auto)

---

Home Index