---

Step * of Lemma es-first-init

∀[es:EO]. ∀[e:E].  (first(es-init(es;e)) ~ tt)
BY
{ Auto }

1
1. es : EO
2. e : E
⊢ first(es-init(es;e)) = tt

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (first(es-init(es;e))  \msim{}  tt)


By

Auto

---

Home Index