Nuprl Lemma : mset_qinc

s:DSet. ((|s| List) ⊆MSet{s})


Proof




Definitions occuring in Statement :  mset: MSet{s} list: List subtype_rel: A ⊆B all: x:A. B[x] dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] mset: MSet{s} uall: [x:A]. B[x] member: t ∈ T dset: DSet so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a
Lemmas referenced :  subtype_quotient list_wf set_car_wf permr_wf permr_equiv_rel dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaEquality dependent_functionElimination because_Cache independent_isectElimination

Latex:
\mforall{}s:DSet.  ((|s|  List)  \msubseteq{}r  MSet\{s\})



Date html generated: 2019_10_16-PM-01_06_25
Last ObjectModification: 2018_09_17-PM-06_16_39

Theory : mset


Home Index