Step
*
of Lemma
has-es-info-type-subtype
∀[T,U:Type]. ∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].
(has-es-info-type(es;e;f;T)) supposing (has-es-info-type(es;e;f;U) and (U ⊆r T))
BY
{ (RepUR ``has-es-info-type`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T,U:Type]. \mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[es:EO+(Message(f))]. \mforall{}[e:E].
(has-es-info-type(es;e;f;T)) supposing (has-es-info-type(es;e;f;U) and (U \msubseteq{}r T))
By
Latex:
(RepUR ``has-es-info-type`` 0 THEN Auto)
Home
Index