Nuprl Lemma : mFOL-sequent-evidence_transitivity2
From uniform evidence that hyps ⇒ y 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: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ 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