---

Step * of Lemma map-tuple_wf_ntuple

∀[n:ℕ]. ∀[f:Top]. ∀[t:n-tuple(n)].  (map-tuple(n;f;t) ∈ n-tuple(n))
BY
{ (InductionOnNat
   THEN RecUnfold `map-tuple` 0
   THEN (RWO "n-tuple-decomp" 0 THENA Auto)
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].  \mforall{}[t:n-tuple(n)].    (map-tuple(n;f;t)  \mmember{}  n-tuple(n))


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `map-tuple`  0
  THEN  (RWO  "n-tuple-decomp"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index