Step
*
of Lemma
es-interface-vals_wf
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[L:E(X) List]. (es-interface-vals(es; X; L) ∈ A List)
BY
{ (Unfold `es-interface-vals` 0 THEN Auto) }
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A:Type]. \mforall{}[X:EClass(A)]. \mforall{}[L:E(X) List].
(es-interface-vals(es; X; L) \mmember{} A List)
By
(Unfold `es-interface-vals` 0 THEN Auto)
Home
Index