---

Step * 1 of Lemma es-opt-prior-val_wf


1. Info : Type
2. T : Type
3. d : T
4. es : EO+(Info)
5. X : EClass(T)
6. e : E
7. ↑e ∈b prior(X)
⊢ prior(X)(e) ∈ E
BY
{ (SubsumeC ⌈E(X)⌉⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  d  :  T
4.  es  :  EO+(Info)
5.  X  :  EClass(T)
6.  e  :  E
7.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
\mvdash{}  prior(X)(e)  \mmember{}  E


By

---

Latex:
(SubsumeC  \mkleeneopen{}E(X)\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index