---

Step * of Lemma mk_mFOLProofNode_wf

∀[T:Type]. ∀[sr:mFOL-sequent() × mFOLRule()]. ∀[subgoals:T List].  (srsubgoals ∈ mFOL-sequent() × mFOLRule() × (T List))
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[T:Type].  \mforall{}[sr:mFOL-sequent()  \mtimes{}  mFOLRule()].  \mforall{}[subgoals:T  List].
    (sr
      subgoals  \mmember{}  mFOL-sequent()  \mtimes{}  mFOLRule()  \mtimes{}  (T  List))


By

ProveWfLemma

---

Home Index