---

Step * 1 of Lemma list_acc_cons_red_lemma


1. v : Top
2. u : Top
3. b : Top
4. f : Top
⊢ list-accum(t,a,h.f[t;a;h];b;[u / v]) ~ list-accum(t,a,h.f[t;a;h];f[v;b;u];v)
BY
{ xxx(Try (RW (AddrC [1] (UnfoldC `list-accum` ANDTHENC ReduceC)) 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  v  :  Top
2.  u  :  Top
3.  b  :  Top
4.  f  :  Top
\mvdash{}  list-accum(t,a,h.f[t;a;h];b;[u  /  v])  \msim{}  list-accum(t,a,h.f[t;a;h];f[v;b;u];v)


By

---

Latex:
xxx(Try  (RW  (AddrC  [1]  (UnfoldC  `list-accum`  ANDTHENC  ReduceC))  0)\mcdot{}  THEN  Auto)xxx

---

Home Index