Nuprl Lemma : mFO-dest-connective_wf

[T:Type]. ∀[F:mFOL() ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[knd:Atom].  (let a,b dest-knd(fmla) in F[a;b] ∈ T?)


Proof




Definitions occuring in Statement :  mFO-dest-connective: mFO-dest-connective mFOL: mFOL() uall: [x:A]. B[x] so_apply: x[s1;s2] unit: Unit member: t ∈ T function: x:A ─→ B[x] union: left right atom: Atom universe: Type
Lemmas :  mFOconnect?_wf bool_wf eqtt_to_assert eq_atom_wf mFOconnect-knd_wf assert_of_eq_atom mFOconnect-left_wf mFOconnect-right_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom it_wf mFOL_wf unit_wf2
\mforall{}[T:Type].  \mforall{}[F:mFOL()  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].  \mforall{}[knd:Atom].
    (let  a,b  =  dest-knd(fmla)  in
      F[a;b]  \mmember{}  T?)



Date html generated: 2015_07_17-AM-07_54_00
Last ObjectModification: 2015_01_27-AM-10_06_35

Home Index