Nuprl Lemma : mFOL-sequent-evidence_wf

[s:mFOL-sequent()]. (mFOL-sequent-evidence(s) ∈ 𝕌')


Proof




Definitions occuring in Statement :  mFOL-sequent-evidence: mFOL-sequent-evidence(s) mFOL-sequent: mFOL-sequent() uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  mFO-uniform-evidence_wf mFOL-sequent-abstract_wf mFOL-sequent_wf
\mforall{}[s:mFOL-sequent()].  (mFOL-sequent-evidence(s)  \mmember{}  \mBbbU{}')



Date html generated: 2015_07_17-AM-07_56_34
Last ObjectModification: 2015_01_27-AM-10_05_16

Home Index