---

Step * 1 of Lemma select-firstn


1. L : Top List
2. n : ℕ
3. x : ℕn
4. ||L|| ≤ n
⊢ firstn(n;L)[x] ~ L[x]
BY
{ xxx(EqCD THEN Try (BLemma `firstn_all`) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  n  :  \mBbbN{}
3.  x  :  \mBbbN{}n
4.  ||L||  \mleq{}  n
\mvdash{}  firstn(n;L)[x]  \msim{}  L[x]


By

---

Latex:
xxx(EqCD  THEN  Try  (BLemma  `firstn\_all`)  THEN  Auto)xxx

---

Home Index