Nuprl Lemma : eager_map_cons_lemma
∀v,u,f:Top. (eager-map(f;[u / v]) ~ eval x = f u in eval r = eager-map(f;v) in [x / r])
Proof
Definitions occuring in Statement :
eager-map: eager-map(f;as),
cons: [a / b],
callbyvalue: callbyvalue,
top: Top,
all: ∀x:A. B[x],
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
eager-map: eager-map(f;as),
so_lambda: so_lambda(x,y,z.t[x; y; z]),
member: t ∈ T,
top: Top,
so_apply: x[s1;s2;s3]
Lemmas referenced :
list_ind_cons_lemma,
istype-void,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :isect_memberEquality_alt,
voidElimination,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality
Latex:
\mforall{}v,u,f:Top. (eager-map(f;[u / v]) \msim{} eval x = f u in eval r = eager-map(f;v) in [x / r])
Date html generated:
2019_06_20-PM-00_38_57
Last ObjectModification:
2019_02_28-PM-01_04_47
Theory : list_0
Home
Index