---

Step * 1 2 1 2 of Lemma event-ordering+_cumulative


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 ∈ x@0:Atom ⟶ if x@0 =a "info" then es-base-E(x) ⟶ T else Top fi 
BY
{ (DepIsectHD 2 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  self:EO  \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  "info"  then  es-base-E(self)  {}\mrightarrow{}  T  else  Top  fi 
3.  x  \mmember{}  EO
4.  x."info"  \mmember{}  es-base-E(x)  {}\mrightarrow{}  T
\mvdash{}  x  \mmember{}  x@0:Atom  {}\mrightarrow{}  if  x@0  =a  "info"  then  es-base-E(x)  {}\mrightarrow{}  T  else  Top  fi 


By

---

Latex:
(DepIsectHD  2  THEN  Auto)

---

Home Index