---

Step * 1 of Lemma in-eclass_wf


1. T : Type
2. X : EClass(Top)
3. eo : EO+(T)
4. e : E
⊢ e ∈b X ∈ 𝔹
BY
{ (RW (AddrC [2] UnfoldTopAbC) 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  X  :  EClass(Top)
3.  eo  :  EO+(T)
4.  e  :  E
\mvdash{}  e  \mmember{}\msubb{}  X  \mmember{}  \mBbbB{}


By

(RW  (AddrC  [2]  UnfoldTopAbC)  0  THEN  Auto)

---

Home Index