---

Step * of Lemma eclass-val_wf2

∀[Info:Type]. ∀[Z:EClass(Top)]. ∀[X:EClass(E(Z))]. ∀[eo:EO+(Info)]. ∀[e:E].  X(e) ∈ E(Z) supposing ↑e ∈b X
BY
{ Auto }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[Z:EClass(Top)].  \mforall{}[X:EClass(E(Z))].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].
    X(e)  \mmember{}  E(Z)  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

Auto

---

Home Index