---

Step * of Lemma cbv-concat-sq

∀[ll:Top List List]. (cbv-concat(ll) ~ concat(ll))
BY
{ Unfolds ``cbv-concat concat`` 0
THEN InductionOnList
THEN Reduce 0
THEN Try (Trivial)
THEN HypSubst' (-1) 0
THEN Thin (-1) }

1
1. u : Top List
2. v : Top List List
⊢ eval x = u in
  eval y = reduce(λl,l'. (l @ l');[];v) in
    x @ y ~ u @ reduce(λl,l'. (l @ l');[];v)

---

Latex:

---

Latex:
\mforall{}[ll:Top  List  List].  (cbv-concat(ll)  \msim{}  concat(ll))


By

---

Latex:
Unfolds  ``cbv-concat  concat``  0
THEN  InductionOnList
THEN  Reduce  0
THEN  Try  (Trivial)
THEN  HypSubst'  (-1)  0
THEN  Thin  (-1)

---

Home Index