1. eo : EO@i' 2. e : E@i 3. a : E@i 4. b : E@i 5. E ⊆r E 6. a = b ∈ E@i 7. e@0 : es-base-E(eo.e) ⊢ ↑(es-dom(eo.e) e@0) ∈ Type
BY { Auto }
1 1. eo : EO@i' 2. e : E@i 3. a : E@i 4. b : E@i 5. E ⊆r E 6. a = b ∈ E@i 7. e@0 : es-base-E(eo.e) ⊢ eo.e ∈ EO
Latex:
1. eo : EO@i'
2. e : E@i
3. a : E@i
4. b : E@i
5. E \msubseteq{}r E
6. a = b@i
7. e@0 : es-base-E(eo.e)
\mvdash{} \muparrow{}(es-dom(eo.e) e@0) \mmember{} Type