---

Step * 2 1 1 1 of Lemma eo-forward-trivial


1. Info : Type
2. eo : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ Info else Top fi 
3. eo ∈ EO
4. eo."info" ∈ es-base-E(eo) ─→ Info
⊢ eo["dom" := eo."dom"] ∈ EO
BY
{ ((GenConclTerm ⌈eo⌉⋅ THEN Auto) THEN All Thin) }

1
1. v : EO@i'
⊢ v["dom" := v."dom"] ∈ EO

---

Latex:



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


By

((GenConclTerm  \mkleeneopen{}eo\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  All  Thin)

---

Home Index