Nuprl Lemma : mFO-dest-quantifier_wf
∀[T:Type]. ∀[F:ℤ ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[isall:𝔹].
  (let v,b = dest-if isall then all else exists(fmla); in
    F[v;b] ∈ T?)
Proof
Definitions occuring in Statement : 
mFO-dest-quantifier: mFO-dest-quantifier, 
mFOL: mFOL()
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s1;s2]
, 
unit: Unit
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
, 
union: left + right
, 
int: ℤ
, 
universe: Type
Lemmas : 
mFOquant?_wf, 
eqtt_to_assert, 
eq_bool_wf, 
mFOquant-isall_wf, 
bool_wf, 
assert_of_eq_bool, 
mFOquant-var_wf, 
mFOquant-body_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
it_wf, 
mFOL_wf, 
unit_wf2
\mforall{}[T:Type].  \mforall{}[F:\mBbbZ{}  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].  \mforall{}[isall:\mBbbB{}].
    (let  v,b  =  dest-if  isall  then  all  else  exists(fmla);  in
        F[v;b]  \mmember{}  T?)
Date html generated:
2015_07_17-AM-07_54_02
Last ObjectModification:
2015_01_27-AM-10_06_43
Home
Index