---

Step * 2 2 of Lemma tuple_wf

.....subterm..... T:t
2:n
1. u : Type
2. v : Type List
3. (||v|| + 1) - 1 ≠ 0
4. ¬(v = [] ∈ (Type List))
5. ∀F:i:ℕ||v|| ⟶ v[i]
     (rec-case(map(λi.F[i];upto(||v||))) of
      [] => ⋅
      a::as =>
       r.if null(as) then a else <a, r> fi  ∈ tuple-type(v))
6. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
7. ¬False
⊢ rec-case(map(λx.F[x + 1];upto((||v|| + 1) - 1))) of
  [] => ⋅
  h::t =>
   r.if null(t) then h else <h, r> fi  ∈ tuple-type(v)
BY
{ (Subst' (||v|| + 1) - 1 ~ ||v|| 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  u  :  Type
2.  v  :  Type  List
3.  (||v||  +  1)  -  1  \mneq{}  0
4.  \mneg{}(v  =  [])
5.  \mforall{}F:i:\mBbbN{}||v||  {}\mrightarrow{}  v[i]
          (rec-case(map(\mlambda{}i.F[i];upto(||v||)))  of
            []  =>  \mcdot{}
            a::as  =>
              r.if  null(as)  then  a  else  <a,  r>  fi    \mmember{}  tuple-type(v))
6.  F  :  i:\mBbbN{}||v||  +  1  {}\mrightarrow{}  [u  /  v][i]
7.  \mneg{}False
\mvdash{}  rec-case(map(\mlambda{}x.F[x  +  1];upto((||v||  +  1)  -  1)))  of
    []  =>  \mcdot{}
    h::t  =>
      r.if  null(t)  then  h  else  <h,  r>  fi    \mmember{}  tuple-type(v)


By

---

Latex:
(Subst'  (||v||  +  1)  -  1  \msim{}  ||v||  0  THEN  Auto)

---

Home Index