---

Step * of Lemma ss-cat_wf

ss-cat{i:l}() ∈ SmallCategory'
BY
{ (ProveWfLemma
   THEN Try (((DSetVars THEN Symmetry) THEN EqTypeCD THEN Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN Try (((MemTypeCD THEN Auto) THEN D 0 THEN Auto))) }

---

Latex:

---

Latex:
ss-cat\{i:l\}()  \mmember{}  SmallCategory'


By

---

Latex:
(ProveWfLemma
  THEN  Try  (((DSetVars  THEN  Symmetry)  THEN  EqTypeCD  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Try  (((MemTypeCD  THEN  Auto)  THEN  D  0  THEN  Auto)))

---

Home Index