---

Step * of Lemma es-prior-interface-vals-property

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[e:E].
  (X(<e) = if e ∈b prior(X) then X(<prior(X)(e)) @ [X(prior(X)(e))] else [] fi  ∈ (A List))
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀Info:Type. ∀es:EO+(Info). ∀A:Type. ∀X:EClass(A). ∀e:E.
  (X(<e) = if e ∈b prior(X) then X(<prior(X)(e)) @ [X(prior(X)(e))] else [] fi  ∈ (A List))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (X(<e)  =  if  e  \mmember{}\msubb{}  prior(X)  then  X(<prior(X)(e))  @  [X(prior(X)(e))]  else  []  fi  )


By

---

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

---

Home Index