---

Step * of Lemma implies-normal-ds

∀ds:x:Id fp-> Type. (∀x∈dom(ds). A=ds(x) ⇒  A ⇒ Normal(ds))
BY
{ (RepUR ``atom-free-decl normal-ds normal-type fpf-all`` 0 THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}ds:x:Id  fp->  Type.  (\mforall{}x\mmember{}dom(ds).  A=ds(x)  {}\mRightarrow{}    A  {}\mRightarrow{}  Normal(ds))


By

---

Latex:
(RepUR  ``atom-free-decl  normal-ds  normal-type  fpf-all``  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index