---

Step * of Lemma dep-eclass_subtype_rel

∀[T:Type]. ∀[A,B:es:EO+(T) ⟶ e:E ⟶ Type].
  EClass(A[es;e]) ⊆r EClass(B[es;e]) supposing ∀es:EO+(T). ∀e:E.  (A[es;e] ⊆r B[es;e])
BY
{ (Unfold `eclass` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A,B:es:EO+(T)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  Type].
    EClass(A[es;e])  \msubseteq{}r  EClass(B[es;e])  supposing  \mforall{}es:EO+(T).  \mforall{}e:E.    (A[es;e]  \msubseteq{}r  B[es;e])


By

---

Latex:
(Unfold  `eclass`  0  THEN  Auto)

---

Home Index