---

Step * 1 1 of Lemma es-local-property_wf


1. Info : Type
2. P : Id ─→ Info List+ ─→ ℙ
3. es : EO+(Info)
4. e : E
⊢ 0 < ||≤loc(e)||
BY
{ (Unfold `es-le-before` 0 THEN Auto') }

---

Latex:



1.  Info  :  Type
2.  P  :  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}
3.  es  :  EO+(Info)
4.  e  :  E
\mvdash{}  0  <  ||\mleq{}loc(e)||


By

(Unfold  `es-le-before`  0  THEN  Auto')

---

Home Index