---

Step * of Lemma append-tuple-shorten-tuple

∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].
  (append-tuple(n;||L|| - n;fst(split-tuple(x;n));shorten-tuple(x;n)) ~ x)
BY
{ (InstLemma `append-tuple-split-tuple` []
   THEN RepeatFor 3 (ParallelLast')
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)
   THEN Try (Trivial)) }

1
1. L : Type List
2. x : tuple-type(L)
3. n : ℕ||L||
4. append-tuple(n;||L|| - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x
⊢ shorten-tuple(x;n) ~ snd(split-tuple(x;n))

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[x:tuple-type(L)].  \mforall{}[n:\mBbbN{}||L||].
    (append-tuple(n;||L||  -  n;fst(split-tuple(x;n));shorten-tuple(x;n))  \msim{}  x)


By

---

Latex:
(InstLemma  `append-tuple-split-tuple`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (Trivial))

---

Home Index