---

Step * 2 1 1 of Lemma until-class-simple-comb


1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. ∀e'<e.∀v:Top. (¬v ∈ Y(e'))
8. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
9. v : Top@i
10. e' : E
11. (e' <loc e)
12. v ∈ Y(e')
13. ∀e''<e.∀w:Top. (w ∈ Y(e'') ⇒ e'' ≤loc e' )
⊢ False
BY
{ (With ⌈e'⌉ (D 7)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  Y  :  EClass(Top)
5.  es  :  EO+(Info)
6.  e  :  E
7.  \mforall{}e'<e.\mforall{}v:Top.  (\mneg{}v  \mmember{}  Y(e'))
8.  class-pred(Y;es;e)  =  (inr  \mcdot{}  )
9.  v  :  Top@i
10.  e'  :  E
11.  (e'  <loc  e)
12.  v  \mmember{}  Y(e')
13.  \mforall{}e''<e.\mforall{}w:Top.  (w  \mmember{}  Y(e'')  {}\mRightarrow{}  e''  \mleq{}loc  e'  )
\mvdash{}  False


By

---

Latex:
(With  \mkleeneopen{}e'\mkleeneclose{}  (D  7)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index