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:
\mforall{}ds:x:Id fp-> Type. (\mforall{}x\mmember{}dom(ds). A=ds(x) {}\mRightarrow{} A {}\mRightarrow{} Normal(ds))
By
(RepUR ``atom-free-decl normal-ds normal-type fpf-all`` 0 THEN Auto THEN BackThruSomeHyp THEN Auto)
Home
Index