Nuprl Lemma : mset_inc
∀g:OCMon. (MSet{g↓set} ⊆r MSet{g↓oset})
Proof
Definitions occuring in Statement :
mset: MSet{s},
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
oset_of_ocmon: g↓oset,
ocmon: OCMon,
dset_of_mon: g↓set
Definitions unfolded in proof :
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
member: t ∈ T,
oset_of_ocmon: g↓oset,
uall: ∀[x:A]. B[x],
guard: {T},
uimplies: b supposing a
Lemmas referenced :
mset_wf,
dset_of_mon_wf,
abdmonoid_dmon,
ocmon_subtype_abdmonoid,
subtype_rel_transitivity,
ocmon_wf,
abdmonoid_wf,
dmon_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
lambdaEquality,
sqequalHypSubstitution,
sqequalRule,
hypothesisEquality,
cut,
lemma_by_obid,
dependent_functionElimination,
thin,
isectElimination,
applyEquality,
hypothesis,
instantiate,
independent_isectElimination
Latex:
\mforall{}g:OCMon. (MSet\{g\mdownarrow{}set\} \msubseteq{}r MSet\{g\mdownarrow{}oset\})
Date html generated:
2016_05_16-AM-08_25_49
Last ObjectModification:
2015_12_28-PM-06_38_35
Theory : polynom_3
Home
Index