---

Step * of Lemma mk_mFOLSequent_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index