---

Step * of Lemma select_firstn

∀[T:Type]. ∀[as:T List]. ∀[n:{0...||as||}]. ∀[i:ℕn].  (firstn(n;as)[i] = as[i] ∈ T)
BY
{ (% Rearrange for induction %
   Assert ⌜∀T:Type. ∀n:ℕ. ∀as:T List.  ((n ≤ ||as||) ⇒ (∀i:ℕn. (firstn(n;as)[i] = as[i] ∈ T)))⌝
THENM (HypBackchain THEN Auto)
) }

1
.....assertion..... 
∀T:Type. ∀n:ℕ. ∀as:T List.  ((n ≤ ||as||) ⇒ (∀i:ℕn. (firstn(n;as)[i] = as[i] ∈ T)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[n:\{0...||as||\}].  \mforall{}[i:\mBbbN{}n].    (firstn(n;as)[i]  =  as[i])


By

---

Latex:
(\%  Rearrange  for  induction  \%
  Assert  \mkleeneopen{}\mforall{}T:Type.  \mforall{}n:\mBbbN{}.  \mforall{}as:T  List.    ((n  \mleq{}  ||as||)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  (firstn(n;as)[i]  =  as[i])))\mkleeneclose{}
THENM  (HypBackchain  THEN  Auto)
)

---

Home Index