---

Step * of Lemma concat-single

∀[l:Top List]. (concat([l]) ~ l)
BY
{ (Unfold `concat` 0 THEN Reduce 0 THEN (D 0 THENA Auto)) }

1
1. l : Top List
⊢ l @ [] ~ l

---

Latex:

---

Latex:
\mforall{}[l:Top  List].  (concat([l])  \msim{}  l)


By

---

Latex:
(Unfold  `concat`  0  THEN  Reduce  0  THEN  (D  0  THENA  Auto))

---

Home Index