---

Step * of Lemma list_acc_cons_red_lemma

∀v,u,b,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
{ (UnivCD THENA Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}v,u,b,f:Top.    (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:
(UnivCD  THENA  Auto)

---

Home Index