---

Step * of Lemma prior-val-pred

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  (X)' es e ~ if pred(e) ∈b X then {X(pred(e))} else (X)' es pred(e) fi  supposing ¬↑first(e)
BY
{ (InstLemma `prior-val-cases` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN SplitOnHypITE -2 
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `prior-val-cases`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  SplitOnHypITE  -2 
  THEN  Auto)

---

Home Index