---

Step * of Lemma normal-da-single

∀[x:Knd]. ∀[T:Type].  Normal(x : T) supposing Dec(T)
BY
{ Auto⋅ }

1
1. x : Knd
2. T : Type
3. Dec(T)
⊢ Normal(x : T)

---

Latex:

---

Latex:
\mforall{}[x:Knd].  \mforall{}[T:Type].    Normal(x  :  T)  supposing  Dec(T)


By

---

Latex:
Auto\mcdot{}

---

Home Index