---

Step * of Lemma strong-subtype-eo-forward-E

∀[eo:EO]. ∀[e:E].  strong-subtype(E;E)
BY
{ ((Unfold `es-E` 0 THEN Folds ``es-base-E es-dom`` 0)
   THEN BasicUniformUnivCD Auto
   THEN (RWO "eo-forward-base-E" 0 THENA Auto)
   THEN BLemma `strong-subtype-set`
   THEN (InstLemma `eo-forward-wf` [⌈eo⌉;⌈e⌉]⋅ THEN Auto)⋅) }

1
1. eo : EO
2. e : {e:es-base-E(eo)| ↑(es-dom(eo) e)} 
3. eo.e ∈ EO
4. e1 : es-base-E(eo)@i
5. ↑(es-dom(eo.e) e1)@i
⊢ ↑(es-dom(eo) e1)

---

Latex:


\mforall{}[eo:EO].  \mforall{}[e:E].    strong-subtype(E;E)


By

((Unfold  `es-E`  0  THEN  Folds  ``es-base-E  es-dom``  0)
  THEN  BasicUniformUnivCD  Auto
  THEN  (RWO  "eo-forward-base-E"  0  THENA  Auto)
  THEN  BLemma  `strong-subtype-set`
  THEN  (InstLemma  `eo-forward-wf`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index