---

Step * 1 of Lemma es-interface-pred_wf


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. x : E(X)@i
⊢ if x ∈b prior(X) then prior(X)(x) else x fi  c≤ x
BY
{ (SplitOnConclITE THEN EAuto 1) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  x  :  E(X)@i
\mvdash{}  if  x  \mmember{}\msubb{}  prior(X)  then  prior(X)(x)  else  x  fi    c\mleq{}  x


By

---

Latex:
(SplitOnConclITE  THEN  EAuto  1)

---

Home Index