---

Step * 2 1 1 1 of Lemma es-prior-interface-cases-sq


1. [Info] : Type
2. X : EClass(Top)@i'
3. es : EO+(Info)@i'
4. e : E@i
5. ¬↑first(e)
6. ¬↑first(e)
7. ¬↑pred(e) ∈b X
8. ¬↑first(e)
9. #(X es pred(e)) = 1 ∈ ℤ
⊢ True ⇒ (↑(#(case last(λe.(#(X es e) =z 1)) pred(e) of inl(e') => {e'} | inr(x) => {}) =z 1))
BY
{ (D (-3) THEN Unfold `in-eclass` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  X  :  EClass(Top)@i'
3.  es  :  EO+(Info)@i'
4.  e  :  E@i
5.  \mneg{}\muparrow{}first(e)
6.  \mneg{}\muparrow{}first(e)
7.  \mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  X
8.  \mneg{}\muparrow{}first(e)
9.  \#(X  es  pred(e))  =  1
\mvdash{}  True  {}\mRightarrow{}  (\muparrow{}(\#(case  last(\mlambda{}e.(\#(X  es  e)  =\msubz{}  1))  pred(e)  of  inl(e')  =>  \{e'\}  |  inr(x)  =>  \{\})  =\msubz{}  1))


By

---

Latex:
(D  (-3)  THEN  Unfold  `in-eclass`  0  THEN  Auto)\mcdot{}

---

Home Index