Step
*
of Lemma
formal-sum_wf
∀[K:RngSig]. ∀[S:Type].  (formal-sum(K;S) ∈ Type)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[K:RngSig].  \mforall{}[S:Type].    (formal-sum(K;S)  \mmember{}  Type)
By
Latex:
ProveWfLemma
Home
Index