---

Step * 1 1 of Lemma eo-restrict_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. P : E ─→ 𝔹
5. es."info" ∈ es-base-E(es) ─→ Info
⊢ es."info" ∈ es-base-E(es["dom" := λe.((es."dom" e) ∧b (P e))]) ─→ Info
BY
{ (RepUR ``es-base-E`` 0 THEN Fold `es-base-E` 0) }

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. P : E ─→ 𝔹
5. es."info" ∈ es-base-E(es) ─→ Info
⊢ es."info" ∈ es-base-E(es) ─→ Info

---

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.  P  :  E  {}\mrightarrow{}  \mBbbB{}
5.  es."info"  \mmember{}  es-base-E(es)  {}\mrightarrow{}  Info
\mvdash{}  es."info"  \mmember{}  es-base-E(es["dom"  :=  \mlambda{}e.((es."dom"  e)  \mwedge{}\msubb{}  (P  e))])  {}\mrightarrow{}  Info


By

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

---

Home Index