---

Step * 1 of Lemma map-tuple-as-tuple


1. n : ℤ
2. n ≠ 1
3. n ≠ 0
4. 0 < n
5. ∀[f:Top]. ∀[t:n-tuple(n - 1)].  (map-tuple(n - 1;f;t) ~ tuple(n - 1;i.f t.i))
6. f : Top
7. t1 : Top
8. t2 : n-tuple(n - 1)
9. v : ℕn - 1 List
⊢ map(λi.(f t2.i);v) ~ map(λi.(f <t1, t2>.i + 1);v)
BY
{ (ListInd (-1)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN EqCD
   THEN Try (Trivial)
   THEN RW (AddrC [2] (RecUnfoldC `select-tuple`)) 0⋅
   THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n  \mneq{}  1
3.  n  \mneq{}  0
4.  0  <  n
5.  \mforall{}[f:Top].  \mforall{}[t:n-tuple(n  -  1)].    (map-tuple(n  -  1;f;t)  \msim{}  tuple(n  -  1;i.f  t.i))
6.  f  :  Top
7.  t1  :  Top
8.  t2  :  n-tuple(n  -  1)
9.  v  :  \mBbbN{}n  -  1  List
\mvdash{}  map(\mlambda{}i.(f  t2.i);v)  \msim{}  map(\mlambda{}i.(f  <t1,  t2>.i  +  1);v)


By

---

Latex:
(ListInd  (-1)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `select-tuple`))  0\mcdot{}
  THEN  AutoSplit)\mcdot{}

---

Home Index