---

Step * of Lemma select0

∀[L:Top]. (L[0] ~ hd(L))
BY
{ (RecUnfold `select` 0 THEN RepUR ``hd pi1`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Top].  (L[0]  \msim{}  hd(L))


By

---

Latex:
(RecUnfold  `select`  0  THEN  RepUR  ``hd  pi1``  0  THEN  Auto)

---

Home Index