---

Step * 1 of Lemma normal-da-single


1. x : Knd
2. T : Type
3. Dec(T)
⊢ Normal(x : T)
BY
{ (UnfoldTopAb 0 THEN Auto) }

---

Latex:



1.  x  :  Knd
2.  T  :  Type
3.  Dec(T)
\mvdash{}  Normal(x  :  T)


By

(UnfoldTopAb  0  THEN  Auto)

---

Home Index