---

Step * of Lemma select_append_back

∀[T:Type]. ∀[as,bs:T List]. ∀[i:{||as||..||as|| + ||bs||-}].  (as @ bs[i] = bs[i - ||as||] ∈ T)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. as : T List
3. bs : T List
4. i : {||as||..||as|| + ||bs||-}
⊢ as @ bs[i] = bs[i - ||as||] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].  \mforall{}[i:\{||as||..||as||  +  ||bs||\msupminus{}\}].    (as  @  bs[i]  =  bs[i  -  ||as||])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index