---

Step * 2 1 of Lemma tuple_wf

.....subterm..... T:t
1: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
⊢ F[0] ∈ u
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1: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{}  F[0]  \mmember{}  u


By

---

Latex:
Auto

---

Home Index