### Nuprl Lemma : list_acc_cons_red_lemma

`∀v,u,b,f:Top.  (list-accum(t,a,h.f[t;a;h];b;[u / v]) ~ list-accum(t,a,h.f[t;a;h];f[v;b;u];v))`

Proof

Definitions occuring in Statement :  list-accum: `list-accum(t,a,h.f[t; a; h];b;L)` cons: `[a / b]` top: `Top` so_apply: `x[s1;s2;s3]` all: `∀x:A. B[x]` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` list-accum: `list-accum(t,a,h.f[t; a; h];b;L)` cons: `[a / b]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]`
Lemmas referenced :  top_wf spread_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis introduction extract_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}v,u,b,f:Top.    (list-accum(t,a,h.f[t;a;h];b;[u  /  v])  \msim{}  list-accum(t,a,h.f[t;a;h];f[v;b;u];v))

Date html generated: 2018_05_21-PM-00_19_13
Last ObjectModification: 2018_05_19-AM-06_59_10

Theory : list_0

Home Index