Nuprl Lemma : tuple2_lemma
∀F:Top. (tuple(2;x.F[x]) ~ <F[0], F[1]>)
Proof
Definitions occuring in Statement :
tuple: tuple(n;i.F[i]),
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
pair: <a, b>,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
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,
top: Top,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3]
Lemmas referenced :
map_cons_lemma,
istype-void,
map_nil_lemma,
list_ind_cons_lemma,
null_cons_lemma,
null_nil_lemma,
list_ind_nil_lemma,
top_wf
Rules used in proof :
lemma_by_obid,
hypothesis,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalRule,
callbyvalueReduce,
sqleReflexivity,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :isect_memberEquality_alt,
voidElimination
Latex:
\mforall{}F:Top. (tuple(2;x.F[x]) \msim{} <F[0], F[1]>)
Date html generated:
2019_06_20-PM-02_03_09
Last ObjectModification:
2019_01_29-AM-10_31_40
Theory : tuples
Home
Index