---

Step * of Lemma es-init-elim2

∀[es:EO]. ∀[e:E].  es-init(es;e) ~ es-init(es;pred(e)) supposing ¬↑first(e)
BY
{ ((UnivCD THENA Auto)
   THEN (RW (AddrC [1] UnfoldTopAbC) 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{}  es-init(es;pred(e))  supposing  \mneg{}\muparrow{}first(e)


By

((UnivCD  THENA  Auto)
  THEN  (RW  (AddrC  [1]  UnfoldTopAbC)  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