---

Step * of Lemma return-class_wf

∀[Info,A:Type]. ∀[x:A].  (return-class(x) ∈ EClass(A))
BY
{ (Unfold `eclass` 0 THEN ProveWfLemma) }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[x:A].    (return-class(x)  \mmember{}  EClass(A))


By

(Unfold  `eclass`  0  THEN  ProveWfLemma)

---

Home Index