---

Step * of Lemma map-upto-length

∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ T].  L = map(f;upto(||L||)) ∈ (T List) supposing ∀i:ℕ||L||. ((f i) = L[i] ∈ T)
BY
{ xxx(InductionOnList THEN Reduce 0 THEN Auto')xxx }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[f:ℕ||v|| ⟶ T]. v = map(f;upto(||v||)) ∈ (T List) supposing ∀i:ℕ||v||. ((f i) = v[i] ∈ T)
5. f : ℕ||v|| + 1 ⟶ T
6. ∀i:ℕ||v|| + 1. ((f i) = [u / v][i] ∈ T)
⊢ [u / v] = map(f;upto(||v|| + 1)) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\mBbbN{}||L||  {}\mrightarrow{}  T].
    L  =  map(f;upto(||L||))  supposing  \mforall{}i:\mBbbN{}||L||.  ((f  i)  =  L[i])


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0  THEN  Auto')xxx

---

Home Index