---

Step * of Lemma corecbar_wf

∀[T:Type]. (corecbar(T) ∈ Type)
BY
{ (Auto THEN Unfold `corecbar` 0 THEN MemCD THEN Auto THEN BLemma `bar-equal-equiv` THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[T:Type].  (corecbar(T)  \mmember{}  Type)


By

---

Latex:
(Auto  THEN  Unfold  `corecbar`  0  THEN  MemCD  THEN  Auto  THEN  BLemma  `bar-equal-equiv`  THEN  Auto)\mcdot{}

---

Home Index