---

Step * of Lemma normal-ds-single

∀x:Id. ∀[T:Type]. (Normal(T) ⇒ Normal(x : T))
BY
{ (Auto THEN D 0 THEN Auto) }

---

Latex:


\mforall{}x:Id.  \mforall{}[T:Type].  (Normal(T)  {}\mRightarrow{}  Normal(x  :  T))


By

(Auto  THEN  D  0  THEN  Auto)

---

Home Index