Nuprl Lemma : mFO-equal_wf
∀[x:mFOL()]. (mFO-equal(x) ∈ mFOL() ─→ 𝔹)
Proof
Definitions occuring in Statement : 
mFO-equal: mFO-equal(x)
, 
mFOL: mFOL()
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
Lemmas : 
mFOL_ind_wf_simple, 
mFOL_wf, 
unit_wf2, 
mFO-dest-atomic_wf, 
eq_atom_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
list-deq_wf, 
int-deq_wf, 
deq_wf, 
list_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
bfalse_wf, 
mFO-dest-connective_wf, 
mFO-dest-quantifier_wf, 
eq_int_wf, 
assert_of_eq_int, 
neg_assert_of_eq_int
\mforall{}[x:mFOL()].  (mFO-equal(x)  \mmember{}  mFOL()  {}\mrightarrow{}  \mBbbB{})
Date html generated:
2015_07_17-AM-07_54_05
Last ObjectModification:
2015_01_27-AM-10_06_34
Home
Index