---

Step * of Lemma eo-strict-forward-ble

∀[Info:Type]. ∀eo:EO+(Info). ∀e:E. ∀a,b:E.  (a ≤loc b ~ a ≤loc b)
BY
{ (Auto
   THEN (InstLemma `eo-strict-forward-E-subtype` [⌜Info⌝;⌜eo⌝;⌜e⌝]⋅ THENA Auto)
   THEN OldAutoBoolCase ⌜a ≤loc b⌝⋅
   THEN (RWO "eo-strict-forward-le" (-1) THENA Auto)
   THEN OldAutoBoolCase ⌜a ≤loc b⌝⋅) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `eo-strict-forward-E-subtype`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}a  \mleq{}loc  b\mkleeneclose{}\mcdot{}
  THEN  (RWO  "eo-strict-forward-le"  (-1)  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}a  \mleq{}loc  b\mkleeneclose{}\mcdot{})

---

Home Index