Step
*
of Lemma
in-eclass_wf
∀[T:Type]. ∀[X:EClass(Top)]. ∀[eo:EO+(T)]. ∀[e:E].  (e ∈b X ∈ 𝔹)
BY
{ Auto }
1
1. T : Type
2. X : EClass(Top)
3. eo : EO+(T)
4. e : E
⊢ e ∈b X ∈ 𝔹
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[X:EClass(Top)].  \mforall{}[eo:EO+(T)].  \mforall{}[e:E].    (e  \mmember{}\msubb{}  X  \mmember{}  \mBbbB{})
By
Latex:
Auto
Home
Index