---

Step * of Lemma cond-class-subtype2

∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)].  (E(Y) ⊆r E([X?Y]))
BY
{ Auto }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
⊢ E(Y) ⊆r E([X?Y])

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[es:EO+(Info)].    (E(Y)  \msubseteq{}r  E([X?Y]))


By

Auto

---

Home Index