---

Step * of Lemma mk_mFOLSequentRule_wf

∀[s:mFOL-sequent()]. ∀[r:mFOLRule()].  (sBY r ∈ mFOL-sequent() × mFOLRule())
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[s:mFOL-sequent()].  \mforall{}[r:mFOLRule()].    (sBY  r  \mmember{}  mFOL-sequent()  \mtimes{}  mFOLRule())


By

ProveWfLemma

---

Home Index