---

Step * of Lemma strictness-concat

concat(⊥) ~ ⊥
BY
{ (RepUR ``concat reduce list_ind`` 0 THEN RW UnrollLoopsOnceC 0 THEN Strictness THEN Auto) }

---

Latex:

---

Latex:
concat(\mbot{})  \msim{}  \mbot{}


By

---

Latex:
(RepUR  ``concat  reduce  list\_ind``  0  THEN  RW  UnrollLoopsOnceC  0  THEN  Strictness  THEN  Auto)

---

Home Index