---

Step * of Lemma es-opt-prior-val_wf

∀[Info,T:Type]. ∀[d:T]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E].  (X'(e)?d ∈ T)
BY
{ ProveWfLemma }

1
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

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[d:T].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].    (X'(e)?d  \mmember{}  T)


By

---

Latex:
ProveWfLemma

---

Home Index