---

Step * of Lemma sq_stable__no-classrel-in-interval

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[start,e:E].  SqStable((no X between start and e))
BY
{ (Auto THEN Unfold `no-classrel-in-interval` 0) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. start : E
6. e : E
⊢ SqStable(∀e'<e.start ≤loc e'  ⇒ (∀w:T. (¬w ∈ X(e'))))

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[start,e:E].    SqStable((no  X  between  start  and  e))


By

(Auto  THEN  Unfold  `no-classrel-in-interval`  0)

---

Home Index