Step * 2 of Lemma mk-extended-eo_wf


1. Info Type@i'
2. Type@i'
3. info E ─→ Info@i
4. EO@i'
5. es-base-E(v) E ∈ Type@i'
⊢ info ∈ es-base-E(v["info" := info]) ─→ Info
BY
(RepUR ``es-base-E`` THEN Fold `es-base-E` 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