---

Step * of Lemma ap2-tuple_wf_ntuple

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

---

Latex:

---

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


By

---

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

---

Home Index