Step
*
of Lemma
eclass_wf2
∀[f:Name ─→ Type]. ∀[T:𝕌'].  (EClass(T) ∈ 𝕌{i''})
BY
{ Auto }
Latex:
Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:\mBbbU{}'].    (EClass(T)  \mmember{}  \mBbbU{}\{i''\})
By
Latex:
Auto
Home
Index