Nuprl Lemma : mFOLisImp_wf

[A:mFOL()]. (mFOLisImp(A) ∈ 𝔹)


Proof




Definitions occuring in Statement :  mFOLisImp: mFOLisImp(A) mFOL: mFOL() bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Lemmas :  mFOconnect?_wf bool_wf eqtt_to_assert eq_atom_wf mFOconnect-knd_wf mFOL_wf
\mforall{}[A:mFOL()].  (mFOLisImp(A)  \mmember{}  \mBbbB{})



Date html generated: 2015_07_17-AM-07_54_51
Last ObjectModification: 2015_01_27-AM-10_06_03

Home Index