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