Nuprl Lemma : tuple1_lemma
∀F:Top. (tuple(1;x.F[x]) ~ F[0])
Proof
Definitions occuring in Statement :
tuple: tuple(n;i.F[i]),
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
tuple: tuple(n;i.F[i]),
upto: upto(n),
from-upto: [n, m),
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
member: t ∈ T,
top: Top,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3]
Lemmas referenced :
istype-top,
map_cons_lemma,
istype-void,
map_nil_lemma,
list_ind_cons_lemma,
null_nil_lemma,
list_ind_nil_lemma
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
cut,
hypothesis,
introduction,
extract_by_obid,
sqequalRule,
callbyvalueReduce,
sqleReflexivity,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :isect_memberEquality_alt,
voidElimination
Latex:
\mforall{}F:Top. (tuple(1;x.F[x]) \msim{} F[0])
Date html generated:
2019_06_20-PM-02_03_07
Last ObjectModification:
2019_01_29-AM-10_15_23
Theory : tuples
Home
Index