Nuprl Lemma : term_accum1_varterm_lemma
∀p,v,M,vcase,Q:Top.
(term-accum1(varterm(v))a,b,c,d.Q[a;b;c;d]varterm(v) with p ⇒ vcase[v;p]mkterm(f,bts) with p ⇒ L.M[p;f;bts;L] p
~ vcase[v;p])
Proof
Definitions occuring in Statement :
term-accum1: term-accum1,
varterm: varterm(v),
top: Top,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
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,v,M,vcase,Q:Top.
(term-accum1(varterm(v))
a,b,c,d.Q[a;b;c;d]
varterm(v) with p {}\mRightarrow{} vcase[v;p]
mkterm(f,bts) with p {}\mRightarrow{} L.M[p;f;bts;L]
p \msim{} vcase[v;p])
Date html generated:
2020_05_19-PM-09_55_05
Last ObjectModification:
2020_03_09-PM-04_08_40
Theory : terms
Home
Index