---

Step * of Lemma C_TYPE-rank_wf

∀[ctyp:C_TYPE()]. (C_TYPE-rank(ctyp) ∈ ℕ)
BY
{ (ProveWfLemma THEN BLemma `non_neg_sum` THEN Auto) }

---

Latex:


\mforall{}[ctyp:C\_TYPE()].  (C\_TYPE-rank(ctyp)  \mmember{}  \mBbbN{})


By

(ProveWfLemma  THEN  BLemma  `non\_neg\_sum`  THEN  Auto)

---

Home Index