---

Step * of Lemma cube-cat_wf

CubeCat ∈ SmallCategory
BY
{ (Unfold `cube-cat` 0 THEN At ⌜Type⌝ MemTypeCD⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
CubeCat  \mmember{}  SmallCategory


By

---

Latex:
(Unfold  `cube-cat`  0  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index