---

Step * of Lemma eclass_wf

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

---

Latex:

---

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


By

---

Latex:
WithCumulativity  ProveWfLemma

---

Home Index