---

Step * of Lemma spread-bag-append

∀[x,F,L:Top].  (let a,b = x in F[a;b] + L ~ let a,b = x in F[a;b] + L)
BY
{ (Auto THEN RepUR ``bag-append append list_ind cons so_apply`` 0 THEN UnrollLoopsOnce) }

---

Latex:

---

Latex:
\mforall{}[x,F,L:Top].    (let  a,b  =  x  in  F[a;b]  +  L  \msim{}  let  a,b  =  x  in  F[a;b]  +  L)


By

---

Latex:
(Auto  THEN  RepUR  ``bag-append  append  list\_ind  cons  so\_apply``  0  THEN  UnrollLoopsOnce)

---

Home Index