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