---

Step * 1 of Lemma sq_stable__no-classrel-in-interval


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'))))
BY
{ (Unfold `alle-lt` 0 THEN Auto THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  start  :  E
6.  e  :  E
\mvdash{}  SqStable(\mforall{}e'<e.start  \mleq{}loc  e'    {}\mRightarrow{}  (\mforall{}w:T.  (\mneg{}w  \mmember{}  X(e'))))


By

(Unfold  `alle-lt`  0  THEN  Auto  THEN  Auto)

---

Home Index