---

Step * of Lemma normal-da_wf

∀[da:k:Knd fp-> Type]. (Normal(da) ∈ ℙ)
BY
{ (RepUR ``normal-da fpf-all`` 0 THEN Auto) }

---

Latex:


\mforall{}[da:k:Knd  fp->  Type].  (Normal(da)  \mmember{}  \mBbbP{})


By

(RepUR  ``normal-da  fpf-all``  0  THEN  Auto)

---

Home Index