---

Step * of Lemma mk_mFOLSequentRule_wf

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

---

Latex:

---

Latex:
\mforall{}[s:mFOL-sequent()].  \mforall{}[r:FOLRule()].    (s  BY  r  \mmember{}  mFOL-sequent()  \mtimes{}  FOLRule())


By

---

Latex:
ProveWfLemma

---

Home Index