---

Step * 1 of Lemma tuple_wf


1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀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))
5. F : i:ℕ||v|| + 1 ⟶ [u / v][i]
6. ¬False
7. ((||v|| + 1) - 1) = 0 ∈ ℤ
⊢ F[0] ∈ u × tuple-type(v)
BY
{ (D 3 THEN DVar `v' THEN All Reduce THEN Auto') }

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mneg{}(v  =  [])
4.  \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))
5.  F  :  i:\mBbbN{}||v||  +  1  {}\mrightarrow{}  [u  /  v][i]
6.  \mneg{}False
7.  ((||v||  +  1)  -  1)  =  0
\mvdash{}  F[0]  \mmember{}  u  \mtimes{}  tuple-type(v)


By

---

Latex:
(D  3  THEN  DVar  `v'  THEN  All  Reduce  THEN  Auto')

---

Home Index