---

Step * 2 of Lemma es-init-identity


1. es : EO
2. e : E
3. ↑first(e)
⊢ es-init(es;e) = e ∈ E
BY
{ (Unfold `es-init` 0
   THEN RecUnfold `final-iterate` 0
   THEN RepUR ``can-apply do-apply`` 0
   THEN (BoolCase ⌈first(e)⌉⋅ THENA Auto)
   THEN RepUR ``bfalse`` 0
   THEN Auto) }

---

Latex:



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


By

(Unfold  `es-init`  0
  THEN  RecUnfold  `final-iterate`  0
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  (BoolCase  \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``bfalse``  0
  THEN  Auto)

---

Home Index