---

Step * of Lemma shorten-tuple_wf

∀[L:Type List]. ∀[n:ℕ||L||]. ∀[x:tuple-type(L)].  (shorten-tuple(x;n) ∈ tuple-type(nth_tl(n;L)))
BY
{ (Auto THEN RWO "shorten-tuple-split-tuple" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[n:\mBbbN{}||L||].  \mforall{}[x:tuple-type(L)].    (shorten-tuple(x;n)  \mmember{}  tuple-type(nth\_tl(n;L)))


By

---

Latex:
(Auto  THEN  RWO  "shorten-tuple-split-tuple"  0  THEN  Auto)

---

Home Index