Step
*
of Lemma
es-interface-subtype_rel
∀[Info,A,B:Type].  EClass(A) ⊆r EClass(B) supposing A ⊆r B
BY
{ Auto }
Latex:
\mforall{}[Info,A,B:Type].    EClass(A)  \msubseteq{}r  EClass(B)  supposing  A  \msubseteq{}r  B
By
Auto
Home
Index