---

Step * of Lemma eclass_wf

∀[T:Type]. ∀[A:es:EO+(T) ─→ E ─→ Type].  (EClass(A[es;e]) ∈ 𝕌')
BY
{ WithCumulativity ProveWfLemma }

---

Latex:


\mforall{}[T:Type].  \mforall{}[A:es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].    (EClass(A[es;e])  \mmember{}  \mBbbU{}')


By

WithCumulativity  ProveWfLemma

---

Home Index