---

Step * 1 2 1 of Lemma eo-restrict_property

.....subterm..... T:t
1:n
1. es : EO@i'
2. P : E ─→ 𝔹@i
⊢ es-base-E(es) ∈ Type
BY
{ Auto }

---

Latex:


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


By

Auto

---

Home Index