---

Step * of Lemma lifting-spread-concat

∀[a,b:Top].  (concat(let x,y = a in b[x;y]) ~ let x,y = a in concat(b[x;y]))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``concat reduce list_ind`` 0 THEN UnrollLoopsOnce) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``concat  reduce  list\_ind``  0  THEN  UnrollLoopsOnce)

---

Home Index