Nuprl Lemma : mFOL-sequent-evidence-trivial
Uniform evidence for a trivially true sequent where the conclusion is
a given member of the hypotheses.⋅
∀hyps:mFOL() List. ∀i:ℕ||hyps||. mFOL-sequent-evidence(<hyps, hyps[i]>)
Proof
Definitions occuring in Statement :
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFOL: mFOL(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
pair: <a, b>,
natural_number: $n
Lemmas :
int_seg_properties,
select-tuple_wf,
non_neg_length,
map_length,
select-map,
subtype_rel_list,
top_wf,
lelt_wf,
FOSatWith_wf,
mFOL-abstract_wf,
select_wf,
tuple-type_wf,
map_wf,
mFOL_wf,
FOAssignment_wf,
FOStruct_wf,
int_seg_wf,
length_wf,
list_wf
\mforall{}hyps:mFOL() List. \mforall{}i:\mBbbN{}||hyps||. mFOL-sequent-evidence(<hyps, hyps[i]>)
Date html generated:
2015_07_17-AM-07_56_36
Last ObjectModification:
2015_01_27-AM-10_06_51
Home
Index