---

Step * of Lemma es-init-identity

∀[es:EO]. ∀[e:E].  uiff(es-init(es;e) = e ∈ E;↑first(e))
BY
{ Auto }

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

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

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    uiff(es-init(es;e)  =  e;\muparrow{}first(e))


By

Auto

---

Home Index