Nuprl Lemma : mset_for_null_lemma
∀f,g,s:Top. (msFor{g} x ∈ 0{s}. f[x] ~ e)
Proof
Definitions occuring in Statement :
mset_for: mset_for,
null_mset: 0{s},
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
sqequal: s ~ t,
grp_id: e
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
mset_for: mset_for,
mon_for: For{g} x ∈ as. f[x],
for: For{T,op,id} x ∈ as. f[x],
reduce: reduce(f;k;as),
list_ind: list_ind,
map: map(f;as),
null_mset: 0{s},
nil: [],
it: ⋅,
grp_id: e,
pi1: fst(t),
pi2: snd(t)
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
hypothesis,
inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid,
sqequalRule
Latex:
\mforall{}f,g,s:Top. (msFor\{g\} x \mmember{} 0\{s\}. f[x] \msim{} e)
Date html generated:
2019_10_16-PM-01_06_33
Last ObjectModification:
2018_10_08-PM-00_46_02
Theory : mset
Home
Index