---

Step * 1 4 2 of Lemma eo-restrict_property

.....subterm..... T:t
2:n
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : {e:es-base-E(es)| ↑(es-dom(es) e)} 
⊢ ↑(P e) ∈ Type
BY
{ (D -1 THEN (Auto THEN MemTypeCD THEN Folds ``es-base-E es-dom`` 0 THEN Auto)) }

---

Latex:


.....subterm.....  T:t
2:n
1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
3.  e  :  \{e:es-base-E(es)|  \muparrow{}(es-dom(es)  e)\} 
\mvdash{}  \muparrow{}(P  e)  \mmember{}  Type


By

(D  -1  THEN  (Auto  THEN  MemTypeCD  THEN  Folds  ``es-base-E  es-dom``  0  THEN  Auto))

---

Home Index