---

Step * of Lemma prior-val-cases

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  ((X)' es e ~ if first(e) then {}
  if pred(e) ∈b X then {X(pred(e))}
  else (X)' es pred(e)
  fi )
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.
  ((X)' es e ~ if first(e) then {}
  if pred(e) ∈b X then {X(pred(e))}
  else (X)' es pred(e)
  fi )

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    ((X)'  es  e  \msim{}  if  first(e)  then  \{\}
    if  pred(e)  \mmember{}\msubb{}  X  then  \{X(pred(e))\}
    else  (X)'  es  pred(e)
    fi  )


By

---

Latex:
(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index