---

Step * of Lemma eo-strict-forward-bless

∀[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-locl" (-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  <loc  b  \msim{}  a  <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  <loc  b\mkleeneclose{}\mcdot{}
  THEN  (RWO  "eo-strict-forward-locl"  (-1)  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}a  <loc  b\mkleeneclose{}\mcdot{})

---

Home Index