---

Step * 1 of Lemma event-ordering+_cumulative

.....subterm..... T:t
1:n
1. T : Type
2. x : EO+(T)@i'
⊢ x ∈ EO+(T)
BY
{ D (-1) }

1
.....aux..... 
1. T : Type
2. x : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ T else Top fi 
3. x ∈ EO
4. x ∈ x@0:Atom ─→ if x@0 =a "info" then es-base-E(x) ─→ T else Top fi 
5. (x "info") = (x "info") ∈ if "info" =a "info" then es-base-E(x) ─→ T else Top fi 
⊢ es-base-E(x) ─→ T ∈ Type

2
1. T : Type
2. x : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ T else Top fi 
3. x ∈ EO
4. x."info" ∈ es-base-E(x) ─→ T
⊢ x ∈ EO+(T)

---

Latex:


.....subterm.....  T:t
1:n
1.  T  :  Type
2.  x  :  EO+(T)@i'
\mvdash{}  x  \mmember{}  EO+(T)


By

D  (-1)

---

Home Index