Nuprl Lemma : mset_inc_a
∀g:OCMon. (MSet{g↓oset} ⊆r MSet{g↓set})
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],
oset_of_ocmon: g↓oset,
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a
Lemmas referenced :
subtype_rel_self,
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,
sqequalRule,
cut,
hypothesis,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
dependent_functionElimination,
hypothesisEquality,
applyEquality,
instantiate,
independent_isectElimination
Latex:
\mforall{}g:OCMon. (MSet\{g\mdownarrow{}oset\} \msubseteq{}r MSet\{g\mdownarrow{}set\})
Date html generated:
2019_10_16-PM-01_09_07
Last ObjectModification:
2018_09_17-PM-06_14_30
Theory : polynom_3
Home
Index