---

Step * of Lemma es-prior-val_wf

∀[Info,T:Type]. ∀[X:EClass(T)].  ((X)' ∈ EClass(T))
BY
{ (Auto THEN Unfold `eclass` 0 THEN ProveWfLemma) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)@i'
5. e : E@i
6. e ∈b prior(X) ∈ 𝔹
7. ↑e ∈b prior(X)
⊢ prior(X)(e) ∈ E

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    ((X)'  \mmember{}  EClass(T))


By

---

Latex:
(Auto  THEN  Unfold  `eclass`  0  THEN  ProveWfLemma)

---

Home Index