---

Step * of Lemma eo-forward-E-subtype

∀[eo:EO]. ∀[e:E].  (E ⊆r E)
BY
{ (Auto THEN RepUR ``es-E eo-forward eo-restrict`` 0 THEN Folds ``es-base-E es-dom`` 0 THEN D 0) }

1
.....subterm..... T:t
1:n
1. eo : EO
2. e : E
3. x : {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} @i
⊢ x ∈ {e:es-base-E(eo)| ↑(es-dom(eo) e)} 

2
.....eq aux..... 
1. eo : EO
2. e : E
⊢ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))}  ∈ Type

---

Latex:


\mforall{}[eo:EO].  \mforall{}[e:E].    (E  \msubseteq{}r  E)


By

(Auto  THEN  RepUR  ``es-E  eo-forward  eo-restrict``  0  THEN  Folds  ``es-base-E  es-dom``  0  THEN  D  0)

---

Home Index