---

Step * 1 2 1 of Lemma split-tuple_wf


1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[x:if null(v) then u1 else u1 × tuple-type(v) fi ]. ∀[n:ℕ||v|| + 1].
     (split-tuple(x;n) ∈ tuple-type(firstn(n;[u1 / v])) × tuple-type(nth_tl(n;[u1 / v])))
5. x1 : u
6. x2 : if null(v) then u1 else u1 × tuple-type(v) fi 
7. n : ℕ(||v|| + 1) + 1
8. ¬(n ≤ 0)
9. n ≠ 1
10. n ≠ 0
11. split-tuple(x2;n - 1) ∈ tuple-type(firstn(n - 1;[u1 / v])) × tuple-type(nth_tl(n - 1;[u1 / v]))
12. v2 : tuple-type(firstn(n - 1;[u1 / v]))
13. v3 : tuple-type(nth_tl(n - 1;[u1 / v]))
14. split-tuple(x2;n - 1) = <v2, v3> ∈ (tuple-type(firstn(n - 1;[u1 / v])) × tuple-type(nth_tl(n - 1;[u1 / v])))
⊢ <x1, v2> ∈ tuple-type(firstn(n;[u; [u1 / v]]))
BY
{ (RecUnfold `firstn` 0 THEN Reduce 0 THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

1.  u  :  Type
2.  u1  :  Type
3.  v  :  Type  List
4.  \mforall{}[x:if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi  ].  \mforall{}[n:\mBbbN{}||v||  +  1].
          (split-tuple(x;n)  \mmember{}  tuple-type(firstn(n;[u1  /  v]))  \mtimes{}  tuple-type(nth\_tl(n;[u1  /  v])))
5.  x1  :  u
6.  x2  :  if  null(v)  then  u1  else  u1  \mtimes{}  tuple-type(v)  fi 
7.  n  :  \mBbbN{}(||v||  +  1)  +  1
8.  \mneg{}(n  \mleq{}  0)
9.  n  \mneq{}  1
10.  n  \mneq{}  0
11.  split-tuple(x2;n  -  1)  \mmember{}  tuple-type(firstn(n  -  1;[u1  /  v]))  \mtimes{}  tuple-type(nth\_tl(n  -  1;[u1  /  v]))
12.  v2  :  tuple-type(firstn(n  -  1;[u1  /  v]))
13.  v3  :  tuple-type(nth\_tl(n  -  1;[u1  /  v]))
14.  split-tuple(x2;n  -  1)  =  <v2,  v3>
\mvdash{}  <x1,  v2>  \mmember{}  tuple-type(firstn(n;[u;  [u1  /  v]]))


By

---

Latex:
(RecUnfold  `firstn`  0  THEN  Reduce  0  THEN  RepeatFor  2  (AutoSplit))

---

Home Index