---

Step * of Lemma normal-ds_wf

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

---

Latex:


\mforall{}[ds:x:Id  fp->  Type].  (Normal(ds)  \mmember{}  \mBbbP{})


By

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

---

Home Index