Nuprl Lemma : mFOL-sequent-evidence_transitivity2

From uniform evidence that hyps  and 
uniform evidence that (y ∧ hyps)  x
we construct uniform evidence that hyps  x.⋅

hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-sequent-evidence(<hyps, y> mFOL-sequent-evidence(<[y hyps], x> mFOL-s\000Cequent-evidence(<hyps, x>))


Proof




Definitions occuring in Statement :  mFOL-sequent-evidence: mFOL-sequent-evidence(s) mFOL: mFOL() cons: [a b] list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q pair: <a, b>
Lemmas :  map_cons_lemma tupletype_cons_lemma mFOL_wf list-cases map_nil_lemma tupletype_nil_lemma null_nil_lemma unit_wf2 product_subtype_list null_cons_lemma null_wf3 map_wf FOSatWith_wf mFOL-abstract_wf subtype_rel_list top_wf bool_wf eqtt_to_assert assert_of_null eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base list_wf tuple-type_wf FOAssignment_wf FOStruct_wf mFOL-sequent-evidence_wf cons_wf
\mforall{}hyps:mFOL()  List
    \mforall{}[x,y:mFOL()].    (mFOL-sequent-evidence(<hyps,  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<[y  /  hyps],  x>)  {}\mRightarrow{}  mFO\000CL-sequent-evidence(<hyps,  x>))



Date html generated: 2015_07_17-AM-07_56_39
Last ObjectModification: 2015_01_27-AM-10_05_26

Home Index