---

Step * 1 1 of Lemma eo-reset-dom_wf_extended


1. Info : Type
2. es : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ Info else Top fi 
3. es ∈ EO
4. d : es-base-E(es) ─→ 𝔹
5. es."info" ∈ es-base-E(es) ─→ Info
⊢ es."info" ∈ es-base-E(es["dom" := d]) ─→ Info
BY
{ (RepUR ``es-base-E`` 0 THEN Fold `es-base-E` 0 THEN Auto) }

---

Latex:



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


By

(RepUR  ``es-base-E``  0  THEN  Fold  `es-base-E`  0  THEN  Auto)

---

Home Index