---

Step * 1 1 of Lemma es-local-property_wf

.....set predicate..... 
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:

---

Latex:
.....set  predicate..... 
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

---

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

---

Home Index