---

Step * of Lemma select_concat_sum

∀[T:Type]. ∀[ll:T List List]. ∀[i:ℕ||ll||]. ∀[j:ℕ||ll[i]||].  (ll[i][j] = concat(ll)[Σ(||ll[k]|| | k < i) + j] ∈ T)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℕ||ll[i]||
⊢ ll[i][j] = concat(ll)[Σ(||ll[k]|| | k < i) + j] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].  \mforall{}[i:\mBbbN{}||ll||].  \mforall{}[j:\mBbbN{}||ll[i]||].
    (ll[i][j]  =  concat(ll)[\mSigma{}(||ll[k]||  |  k  <  i)  +  j])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index