---

Step * of Lemma prior-val-first

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].  (X)' es e ~ {} supposing ↑first(e)
BY
{ ((UnivCD THENA Auto) THEN (RWO "prior-val-cases" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].    (X)'  es  e  \msim{}  \{\}  supposing  \muparrow{}first(e)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "prior-val-cases"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index