---

Step * of Lemma select_append_front

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

1
1. T : Type
2. as : T List
3. bs : T List
4. i : ℕ||as||
⊢ as @ bs[i] = as[i] ∈ T

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index