---

Step * of Lemma FOL-hyps-meaning_wf

∀[concl:mFOL()]. ∀[hyps:mFOL() List]. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀[a:FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)].
  (FOL-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+\{i:l\}(Dom)].
\mforall{}[a:FOAssignment(mFOL-sequent-freevars(<hyps,  concl>),Dom)].
    (FOL-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