Step
*
of Lemma
mFOL-sequent-evidence_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-evidence(s) ∈ 𝕌')
BY
{ ProveWfLemma }
Latex:
\mforall{}[s:mFOL-sequent()].  (mFOL-sequent-evidence(s)  \mmember{}  \mBbbU{}')
By
ProveWfLemma
Home
Index