---

Step * of Lemma eager-append-is-append

∀[as,bs:Top List].  (eager-append(as;bs) ~ as @ bs)
BY
{ (InductionOnList THEN Unfold `eager-append` 0 THEN Reduce  0 THEN Auto THEN Fold `eager-append` 0 THEN Auto) }

1
1. u : Top
2. v : Top List
3. ∀[bs:Top List]. (eager-append(v;bs) ~ v @ bs)
4. bs : Top List
⊢ eval r' = eager-append(v;bs) in
  [u / r'] ~ [u / (v @ bs)]

---

Latex:

---

Latex:
\mforall{}[as,bs:Top  List].    (eager-append(as;bs)  \msim{}  as  @  bs)


By

---

Latex:
(InductionOnList
  THEN  Unfold  `eager-append`  0
  THEN  Reduce    0
  THEN  Auto
  THEN  Fold  `eager-append`  0
  THEN  Auto)

---

Home Index