---

Step * of Lemma member-eclass_wf

∀[T,U:Type]. ∀[X:EClass(U)]. ∀[es:EO+(T)]. ∀[e:E].  (e ∈b X ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[T,U:Type].  \mforall{}[X:EClass(U)].  \mforall{}[es:EO+(T)].  \mforall{}[e:E].    (e  \mmember{}\msubb{}  X  \mmember{}  \mBbbB{})


By

ProveWfLemma

---

Home Index