Nuprl Lemma : mset_on_grp_eq
∀g:Top. (MSet{g↓set} ~ MSet{g↓oset})
Proof
Definitions occuring in Statement :
mset: MSet{s},
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t,
oset_of_ocmon: g↓oset,
dset_of_mon: g↓set
Definitions unfolded in proof :
mset: MSet{s},
dset_of_mon: g↓set,
set_car: |p|,
pi1: fst(t),
oset_of_ocmon: g↓oset,
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}g:Top. (MSet\{g\mdownarrow{}set\} \msim{} MSet\{g\mdownarrow{}oset\})
Date html generated:
2016_05_16-AM-08_25_47
Last ObjectModification:
2015_12_28-PM-06_38_33
Theory : polynom_3
Home
Index