---

Step * of Lemma last-es-le-before

∀es:EO. ∀e:E.  (last(≤loc(e)) = e ∈ E)
BY
{ (Auto
   THEN Unfold `es-le-before` 0
   THEN (RWO "last_append" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN RWO "last_singleton2" 0
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.    (last(\mleq{}loc(e))  =  e)


By

(Auto
  THEN  Unfold  `es-le-before`  0
  THEN  (RWO  "last\_append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "last\_singleton2"  0
  THEN  Auto)

---

Home Index