---

Step * of Lemma mk_mFOLSequent_wf

∀[hyps:mFOL() List]. ∀[concl:mFOL()].  (hyps⊢ concl ∈ mFOL-sequent())
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[hyps:mFOL()  List].  \mforall{}[concl:mFOL()].    (hyps\mvdash{}  concl  \mmember{}  mFOL-sequent())


By

ProveWfLemma

---

Home Index