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