---

Step * of Lemma select_append

∀[T:Type]. ∀[as,bs:T List]. ∀[i:ℕ||as|| + ||bs||].  (as @ bs[i] = if i <z ||as|| then as[i] else bs[i - ||as||] fi  ∈ T)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].  \mforall{}[i:\mBbbN{}||as||  +  ||bs||].
    (as  @  bs[i]  =  if  i  <z  ||as||  then  as[i]  else  bs[i  -  ||as||]  fi  )


By

---

Latex:
Auto

---

Home Index