Nuprl Lemma : dest_mk_prec_lemma
∀x,lbl:Top. (dest-prec(mk-prec(lbl;x)) ~ <lbl, x>)
Proof
Definitions occuring in Statement :
dest-prec: dest-prec(x),
mk-prec: mk-prec(lbl;x),
top: Top,
all: ∀x:A. B[x],
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
dest-prec: dest-prec(x),
mk-prec: mk-prec(lbl;x),
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}x,lbl:Top. (dest-prec(mk-prec(lbl;x)) \msim{} <lbl, x>)
Date html generated:
2019_06_20-PM-02_05_20
Last ObjectModification:
2019_02_22-PM-06_29_34
Theory : tuples
Home
Index