---

Step * 2 of Lemma mk-extended-eo_wf


1. Info : Type@i'
2. E : Type@i'
3. info : E ─→ Info@i
4. v : EO@i'
5. es-base-E(v) = E ∈ Type@i'
⊢ info ∈ es-base-E(v["info" := info]) ─→ Info
BY
{ (RepUR ``es-base-E`` 0 THEN Fold `es-base-E` 0 THEN Auto) }

---

Latex:



1.  Info  :  Type@i'
2.  E  :  Type@i'
3.  info  :  E  {}\mrightarrow{}  Info@i
4.  v  :  EO@i'
5.  es-base-E(v)  =  E@i'
\mvdash{}  info  \mmember{}  es-base-E(v["info"  :=  info])  {}\mrightarrow{}  Info


By

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

---

Home Index