---

Step * of Lemma eo-forward-E-subtype2

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].  ({e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' }  ⊆r E)
BY
{ (Auto
   THEN RWO "eo-forward-E" 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try ((Unfold `es-E` 0 THEN Folds ``es-base-E es-dom`` 0 THEN Auto)⋅)) }

1
.....subterm..... T:t
1:n
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } @i
⊢ x ∈ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} 

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].    (\{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  \}    \msubseteq{}r  E)


By

(Auto
  THEN  RWO  "eo-forward-E"  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  ((Unfold  `es-E`  0  THEN  Folds  ``es-base-E  es-dom``  0  THEN  Auto)\mcdot{}))

---

Home Index