---

Step * 1 of Lemma eager-append-is-append


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)]
BY
{ (CallByValueReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[bs:Top  List].  (eager-append(v;bs)  \msim{}  v  @  bs)
4.  bs  :  Top  List
\mvdash{}  eval  r'  =  eager-append(v;bs)  in
    [u  /  r']  \msim{}  [u  /  (v  @  bs)]


By

---

Latex:
(CallByValueReduce  0  THEN  Auto)

---

Home Index