---

Step * of Lemma eo-strict-forward-le

∀[Info:Type]. ∀eo:EO+(Info). ∀e:E. ∀a,b:E.  (a ≤loc b  ⇐⇒ a ≤loc b )
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``es-le es-locl`` 0
   THEN (RWO "eo-strict-forward-loc" 0 THENA Auto)
   THEN (RWO "eo-strict-forward-less" 0 THENA Auto)
   THEN InstLemma `eo-strict-forward-E-subtype` [⌈Info⌉;⌈eo⌉;⌈e⌉]⋅
   THEN Auto
   THEN ParallelLast
   THEN Auto
   THEN StrongHypSubst (-1) 0
   THEN Auto
   THEN BLemma `member-eo-strict-forward-E` 
   THEN Auto
   THEN InstLemma `eo-strict-forward-E-member` [⌈Info⌉;⌈eo⌉;⌈e⌉;⌈b⌉]⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}eo:EO+(Info).  \mforall{}e:E.  \mforall{}a,b:E.    (a  \mleq{}loc  b    \mLeftarrow{}{}\mRightarrow{}  a  \mleq{}loc  b  )


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-le  es-locl``  0
  THEN  (RWO  "eo-strict-forward-loc"  0  THENA  Auto)
  THEN  (RWO  "eo-strict-forward-less"  0  THENA  Auto)
  THEN  InstLemma  `eo-strict-forward-E-subtype`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  StrongHypSubst  (-1)  0
  THEN  Auto
  THEN  BLemma  `member-eo-strict-forward-E` 
  THEN  Auto
  THEN  InstLemma  `eo-strict-forward-E-member`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index