---

Step * of Lemma es-init-elim

∀[es:EO]. ∀[e:E].  es-init(es;e) ~ e supposing ↑first(e)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-init` 0
   THEN RecUnfold `final-iterate` 0
   THEN RepUR ``can-apply do-apply`` 0
   THEN AutoSplit
   THEN Try (Fold `es-init` 0)
   THEN RepUR ``bfalse`` 0
   THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `es-init`  0
  THEN  RecUnfold  `final-iterate`  0
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  AutoSplit
  THEN  Try  (Fold  `es-init`  0)
  THEN  RepUR  ``bfalse``  0
  THEN  Auto)

---

Home Index