---

Step * of Lemma select-tuple_wf

∀[L:Type List]. ∀[n:ℕ]. ∀[k:ℤ].  ∀[x:tuple-type(L)]. (x.n ∈ L[n]) supposing n < ||L|| ∧ (k = ||L|| ∈ ℤ)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN Eliminate ⌜k⌝⋅ THEN ThinVar `k') }

1
1. v : Type List
2. u : Type
3. ∀[n:ℕ]. ∀[k:ℤ].  ∀[x:tuple-type(v)]. (x.n ∈ v[n]) supposing n < ||v|| ∧ (k = ||v|| ∈ ℤ)
4. n : ℕ
5. n < ||v|| + 1
6. x : if null(v) then u else u × tuple-type(v) fi 
⊢ x.n ∈ [u / v][n]

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbZ{}].    \mforall{}[x:tuple-type(L)].  (x.n  \mmember{}  L[n])  supposing  n  <  ||L||  \mwedge{}  (k  =  ||L||)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}  THEN  ThinVar  `k')

---

Home Index