---

Step * of Lemma mFOL-hyps-meaning_wf

∀[concl:mFOL()]. ∀[hyps:mFOL() List]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(mFOL-sequent-freevars(<hyps
                                                                                                              , concl
                                                                                                              >),Dom)].
  (mFOL-hyps-meaning(Dom;S;a;hyps) ∈ Type List)
BY
{ (Auto THEN (Assert hyps ∈ {h:mFOL()| (h ∈ hyps)}  List BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[concl:mFOL()].  \mforall{}[hyps:mFOL()  List].  \mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].
\mforall{}[a:FOAssignment(mFOL-sequent-freevars(<hyps,  concl>),Dom)].
    (mFOL-hyps-meaning(Dom;S;a;hyps)  \mmember{}  Type  List)


By

---

Latex:
(Auto  THEN  (Assert  hyps  \mmember{}  \{h:mFOL()|  (h  \mmember{}  hyps)\}    List  BY  Auto)  THEN  ProveWfLemma)

---

Home Index