---

Step * 1 of Lemma is-prior-class-when


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. d : Top
6. e : E
⊢ e ∈b (X'?d) when Y ~ e ∈b Y
BY
{ (((Unfold `es-prior-class-when` 0 THEN RW (AddrC [1] UnfoldTopAbC) 0) THEN Reduce 0) THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  Y  :  EClass(Top)
5.  d  :  Top
6.  e  :  E
\mvdash{}  e  \mmember{}\msubb{}  (X'?d)  when  Y  \msim{}  e  \mmember{}\msubb{}  Y


By

---

Latex:
(((Unfold  `es-prior-class-when`  0  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0)  THEN  Reduce  0)
  THEN  RepeatFor  2  (AutoSplit)
  )

---

Home Index