Nuprl Lemma : term_accum_varterm_lemma
∀p,M,v,varcase,Q:Top.
(term-accum(varterm(v) with p)
p,f,vs,xxx.Q[p;f;vs;xxx]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ xxx.M[p;f;bts;xxx] ~ varcase[p;v])
Proof
Definitions occuring in Statement :
term-accum: term-accum,
varterm: varterm(v),
top: Top,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
term-accum: term-accum,
term-accum1: term-accum1,
genrec-ap: genrec-ap,
varterm: varterm(v),
so_apply: x[s1;s2],
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
because_Cache,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}p,M,v,varcase,Q:Top.
(term-accum(varterm(v) with p)
p,f,vs,xxx.Q[p;f;vs;xxx]
varterm(x) with p {}\mRightarrow{} varcase[p;x]
mkterm(f,bts) with p {}\mRightarrow{} xxx.M[p;f;bts;xxx] \msim{} varcase[p;v])
Date html generated:
2020_05_19-PM-09_55_16
Last ObjectModification:
2020_03_09-PM-04_08_46
Theory : terms
Home
Index