---

Step * 1 3 3 1 of Lemma eo-restrict_property


1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑(es-dom(es) x)@i
5. ↑(P x)@i
6. e : es-base-E(es)
7. ↑(es-dom(es) e)
⊢ ↑(P e) ∈ Type
BY
{ (Auto THEN MemTypeCD THEN Folds ``es-base-E es-dom`` 0 THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
3.  x  :  es-base-E(es)@i
4.  \muparrow{}(es-dom(es)  x)@i
5.  \muparrow{}(P  x)@i
6.  e  :  es-base-E(es)
7.  \muparrow{}(es-dom(es)  e)
\mvdash{}  \muparrow{}(P  e)  \mmember{}  Type


By

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

---

Home Index