Nuprl Lemma : mFOL-sequent-evidence-trivial

Uniform evidence for trivially true sequent where the conclusion is
given member of the hypotheses.⋅

hyps:mFOL() List. ∀i:ℕ||hyps||.  mFOL-sequent-evidence(<hyps, hyps[i]>)


Definitions occuring in Statement :  mFOL-sequent-evidence: mFOL-sequent-evidence(s) mFOL: mFOL() select: L[n] length: ||as|| list: 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