---

Step * of Lemma eclass-cond_wf

∀[Info,B:Type]. ∀[X:EClass(B ⟶ B)]. ∀[Y:EClass(B)].  (eclass-cond(X;Y) ∈ EClass(B))
BY
{ (ProveWfLemma THEN (Unfold `eclass` 0 THEN MemCD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[Y:EClass(B)].    (eclass-cond(X;Y)  \mmember{}  EClass(B))


By

---

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

---

Home Index