---

Step * of Lemma map-tuple-ap2-tuple

∀[n:ℕ]. ∀[f,x:Top]. ∀[g,t:n-tuple(n)].
  (map-tuple(n;f;ap2-tuple(n;g;x;t)) ~ ap2-tuple(n;map-tuple(n;λh,x,z. (f (h x z));g);x;t))
BY
{ (Auto
   THEN (RWW "ap2-tuple-as-tuple map-tuple-tuple map-tuple-as-tuple" 0 THENA Auto)
   THEN RepUR ``tuple`` 0
   THEN EqCD
   THEN Try (Trivial)
   THEN Fold `tuple` 0
   THEN GenConclAtAddr [2;2]
   THEN Thin (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN EqCD
   THEN Try (Trivial)
   THEN (RWO "select-tuple-tuple" 0 THENA Auto)
   THEN Reduce 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,x:Top].  \mforall{}[g,t:n-tuple(n)].
    (map-tuple(n;f;ap2-tuple(n;g;x;t))  \msim{}  ap2-tuple(n;map-tuple(n;\mlambda{}h,x,z.  (f  (h  x  z));g);x;t))


By

---

Latex:
(Auto
  THEN  (RWW  "ap2-tuple-as-tuple  map-tuple-tuple  map-tuple-as-tuple"  0  THENA  Auto)
  THEN  RepUR  ``tuple``  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  Fold  `tuple`  0
  THEN  GenConclAtAddr  [2;2]
  THEN  Thin  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  (RWO  "select-tuple-tuple"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Trivial)

---

Home Index