---

Step * 1 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) ─→ Info
BY
{ 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.  P  :  E  {}\mrightarrow{}  \mBbbB{}
5.  es."info"  \mmember{}  es-base-E(es)  {}\mrightarrow{}  Info
\mvdash{}  es."info"  \mmember{}  es-base-E(es)  {}\mrightarrow{}  Info


By

Auto

---

Home Index