---

Step * 1 2 1 1 2 of Lemma lg-remove-noop


1. T : Type
2. x : ℕ
3. v : ℕ@i
4. L : (T × ℕv List × (ℕv List)) List@i
5. v ≤ x@i
6. ||L|| ≤ x@i
⊢ firstn(x;L) @ [] ~ L
BY
{ (RWW "firstn_all append-nil" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  \mBbbN{}
3.  v  :  \mBbbN{}@i
4.  L  :  (T  \mtimes{}  \mBbbN{}v  List  \mtimes{}  (\mBbbN{}v  List))  List@i
5.  v  \mleq{}  x@i
6.  ||L||  \mleq{}  x@i
\mvdash{}  firstn(x;L)  @  []  \msim{}  L


By

---

Latex:
(RWW  "firstn\_all  append-nil"  0  THEN  Auto)

---

Home Index