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:
Latex:
\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[es:EO+(Info)].    (E(Y)  \msubseteq{}r  E([X?Y]))
By
Latex:
Auto
Home
Index