Step * of Lemma es-first-init

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

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


Latex:


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


By


Latex:
Auto




Home Index