Nuprl Lemma : mk_mFOLSequent_wf
∀[hyps:mFOL() List]. ∀[concl:mFOL()]. (hyps⊢ concl ∈ mFOL-sequent())
Proof
Definitions occuring in Statement :
mk_mFOLSequent: mk_mFOLSequent,
mFOL-sequent: mFOL-sequent(),
mFOL: mFOL(),
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
mFOL_wf,
list_wf
\mforall{}[hyps:mFOL() List]. \mforall{}[concl:mFOL()]. (hyps\mvdash{} concl \mmember{} mFOL-sequent())
Date html generated:
2015_07_17-AM-07_56_27
Last ObjectModification:
2015_01_27-AM-10_05_09
Home
Index