---

Step * of Lemma split-tuple_wf

∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].  (split-tuple(x;n) ∈ tuple-type(firstn(n;L)) × tuple-type(nth_tl(n;L)))
BY
{ (InductionOnList
   THEN (UnivCD THENA Auto)
   THEN All Reduce
   THEN Auto
   THEN RecUnfold `split-tuple` 0
   THEN (AutoSplit
         THENL [TACTIC:((HypSubst' (-1) 0 THEN RWO "first0" 0) THEN Reduce 0 THEN Auto)
               ; (DVar `v' THENL [TACTIC:Auto'; TACTIC:Id])]
   )) }

1
1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[x:tuple-type([u1 / v])]. ∀[n:ℕ||[u1 / v]||].
     (split-tuple(x;n) ∈ tuple-type(firstn(n;[u1 / v])) × tuple-type(nth_tl(n;[u1 / v])))
5. x : if null([u1 / v]) then u else u × tuple-type([u1 / v]) fi 
6. n : ℕ||[u1 / v]|| + 1
7. n ≠ 0
⊢ if (n =z 1) then <fst(x), snd(x)> else let a,b = split-tuple(snd(x);n - 1) in <<fst(x), a>, b> fi 
  ∈ tuple-type(firstn(n;[u; [u1 / v]])) × tuple-type(nth_tl(n;[u; [u1 / v]]))

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  (UnivCD  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto
  THEN  RecUnfold  `split-tuple`  0
  THEN  (AutoSplit
              THENL  [TACTIC:((HypSubst'  (-1)  0  THEN  RWO  "first0"  0)  THEN  Reduce  0  THEN  Auto)
                          ;  (DVar  `v'  THENL  [TACTIC:Auto';  TACTIC:Id])]
  ))

---

Home Index