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