---

Step * 1 of Lemma eo-reset-dom_wf_extended


1. Info : Type
2. es : EO+(Info)
3. d : es-base-E(es) ─→ 𝔹
4. es ∈ EO
⊢ eo-reset-dom(es;d)."info" ∈ es-base-E(eo-reset-dom(es;d)) ─→ Info
BY
{ (Thin (-1) THEN (Unfold `eo-reset-dom` 0 THEN Reduce 0 THEN DRecord 2 ⋅ THEN Auto)⋅) }

1
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

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  d  :  es-base-E(es)  {}\mrightarrow{}  \mBbbB{}
4.  es  \mmember{}  EO
\mvdash{}  eo-reset-dom(es;d)."info"  \mmember{}  es-base-E(eo-reset-dom(es;d))  {}\mrightarrow{}  Info


By

(Thin  (-1)  THEN  (Unfold  `eo-reset-dom`  0  THEN  Reduce  0  THEN  DRecord  2  \mcdot{}  THEN  Auto)\mcdot{})

---

Home Index