Nuprl Lemma : lapp_mon_wf

s:DSet. (<List, @> ∈ Mon)


Proof




Definitions occuring in Statement :  lapp_mon: <List, @> all: x:A. B[x] member: t ∈ T mon: Mon dset: DSet
Definitions unfolded in proof :  all: x:A. B[x] lapp_mon: <List, @> uall: [x:A]. B[x] member: t ∈ T dset: DSet uimplies: supposing a assoc: Assoc(T;op) infix_ap: y top: Top ident: Ident(T;op;id) append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] and: P ∧ Q cand: c∧ B
Lemmas referenced :  mk_mon list_wf set_car_wf eq_list_wf btrue_wf append_wf nil_wf dset_wf append_assoc list_ind_nil_lemma append_back_nil
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaEquality dependent_functionElimination because_Cache independent_isectElimination sqequalRule isect_memberEquality voidElimination voidEquality isect_memberFormation_alt inhabitedIsType axiomEquality equalityTransitivity equalitySymmetry universeIsType independent_pairFormation productElimination independent_pairEquality

Latex:
\mforall{}s:DSet.  (<s  List,  @>  \mmember{}  Mon)



Date html generated: 2019_10_16-PM-01_03_04
Last ObjectModification: 2018_09_26-PM-08_14_32

Theory : list_2


Home Index