---

Step * of Lemma eo-forward-no-prior-classrel

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[start:E]. ∀[e:E].
  uiff((no X prior to e);(no X between start and e)) supposing loc(e) = loc(start) ∈ Id
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0
   THEN ParallelLast
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN All (RWO "eo-forward-locl")⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[start:E].  \mforall{}[e:E].
    uiff((no  X  prior  to  e);(no  X  between  start  and  e))  supposing  loc(e)  =  loc(start)


By

(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0
  THEN  ParallelLast
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  All  (RWO  "eo-forward-locl")\mcdot{}
  THEN  Auto)

---

Home Index