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