---

Step * 1 of Lemma es-init-identity


1. es : EO
2. e : E
3. es-init(es;e) = e ∈ E
⊢ ↑first(e)
BY
{ ((RevHypSubst (-1) 0 THEN Auto) THEN RWO "es-first-init" 0 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  es-init(es;e)  =  e
\mvdash{}  \muparrow{}first(e)


By

((RevHypSubst  (-1)  0  THEN  Auto)  THEN  RWO  "es-first-init"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index