---

Step * of Lemma cond-class_wf

∀[Info,A:Type]. ∀[X,Y:EClass(A)].  ([X?Y] ∈ EClass(A))
BY
{ ProveWfLemma⋅ }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].    ([X?Y]  \mmember{}  EClass(A))


By

ProveWfLemma\mcdot{}

---

Home Index