---

Step * 2 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) @ [n - 1]))
BY
{ ((RWO "map_append_sq" 0 THENA Auto) THEN Reduce 0) }

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


By

---

Latex:
((RWO  "map\_append\_sq"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index