---

Step * 1 2 2 of Lemma eo-restrict_property

.....subterm..... T:t
2:n
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : es-base-E(es)
⊢ ↑((es-dom(es) e) ∧b (P e)) ∈ Type
BY
{ (BoolCase ⌈es-dom(es) e⌉⋅ THENA Auto) }

1
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : es-base-E(es)
4. ↑(es-dom(es) e)
⊢ ↑(P e) ∈ Type

2
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : es-base-E(es)
4. ¬↑(es-dom(es) e)
⊢ False ∈ Type

---

Latex:


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


By

(BoolCase  \mkleeneopen{}es-dom(es)  e\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index