---

Step * of Lemma eo-forward-le-subtype

∀es:EO. ∀e:E. ∀a:E.  ({e1:E| e1 ≤loc a }  ⊆r {e1:E| e1 ≤loc a } )
BY
{ (InstLemma `eo-forward-le` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (InstLemma `eo-forward-wf` [⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN D -1
   THEN MemTypeCD
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.  \mforall{}a:E.    (\{e1:E|  e1  \mleq{}loc  a  \}    \msubseteq{}r  \{e1:E|  e1  \mleq{}loc  a  \}  )


By

(InstLemma  `eo-forward-le`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (InstLemma  `eo-forward-wf`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index