Nuprl Lemma : mset_for_elim_lemma
∀F,as,g,s:Top. (msFor{g} x ∈ mk_mset(as). F[x] ~ For{g} x ∈ as. F[x])
Proof
Definitions occuring in Statement :
mset_for: mset_for,
mk_mset: mk_mset(as),
mon_for: For{g} x ∈ as. f[x],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
sqequal: s ~ t,
set_car: |p|
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
mk_mset: mk_mset(as),
mset_for: mset_for
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
hypothesis,
lemma_by_obid
Latex:
\mforall{}F,as,g,s:Top. (msFor\{g\} x \mmember{} mk\_mset(as). F[x] \msim{} For\{g\} x \mmember{} as. F[x])
Date html generated:
2016_05_16-AM-07_47_47
Last ObjectModification:
2015_12_28-PM-06_02_44
Theory : mset
Home
Index