---

Step * of Lemma es-before-is-nil-if-first

∀[es:EO]. ∀[e:E].  before(e) ~ [] supposing ↑first(e)
BY
{ (Auto THEN RecUnfold `es-before` 0⋅ THEN AutoSplit⋅) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    before(e)  \msim{}  []  supposing  \muparrow{}first(e)


By

(Auto  THEN  RecUnfold  `es-before`  0\mcdot{}  THEN  AutoSplit\mcdot{})

---

Home Index