---

Step * of Lemma firstn_append_front

∀[L1:Top List]. ∀L2:Top List. (firstn(||L1 @ L2|| - ||L2||;L1 @ L2) ~ L1)
BY
{ Auto }

1
1. L1 : Top List
2. L2 : Top List@i
⊢ firstn(||L1 @ L2|| - ||L2||;L1 @ L2) ~ L1

---

Latex:

---

Latex:
\mforall{}[L1:Top  List].  \mforall{}L2:Top  List.  (firstn(||L1  @  L2||  -  ||L2||;L1  @  L2)  \msim{}  L1)


By

---

Latex:
Auto

---

Home Index