---

Step * 2 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. v ∈ Prior(Y)(e)@i
⊢ False
BY
{ ((RWO "primed-classrel" (-1) THEN Auto)⋅ THEN RepeatFor 3 (D -1)) }

1
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

---

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.  v  \mmember{}  Prior(Y)(e)@i
\mvdash{}  False


By

---

Latex:
((RWO  "primed-classrel"  (-1)  THEN  Auto)\mcdot{}  THEN  RepeatFor  3  (D  -1))

---

Home Index