---

Step * 1 of Lemma h-level_wf


1. n : ℤ
⊢ ∀[X:j⊢]. ∀[A:{X ⊢ _}].  X ⊢ Contractible(A)
BY
{ Auto }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    X  \mvdash{}  Contractible(A)


By

---

Latex:
Auto

---

Home Index