---

Step * of Lemma prior-class-when-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)]. ∀[d:Top]. ∀[e:E].
  (X'?d) when Y(e) ~ <Y(e), if e ∈b (X)' then (X)'(e) else d fi > supposing ↑e ∈b (X'?d) when Y
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN Unfold `es-prior-class-when` 0
   THEN RW (AddrC [1;1] UnfoldTopAbC) 0
   THEN RW (AddrC [2;1] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].  \mforall{}[d:Top].  \mforall{}[e:E].
    (X'?d)  when  Y(e)  \msim{}  <Y(e),  if  e  \mmember{}\msubb{}  (X)'  then  (X)'(e)  else  d  fi  >  supposing  \muparrow{}e  \mmember{}\msubb{}  (X'?d)  when  Y


By

---

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

---

Home Index