Nuprl Lemma : ss_ap_id_lemma
∀x:Top. (ss-id()(x) ~ x)
Proof
Definitions occuring in Statement :
ss-id: ss-id(),
ss-ap: f(x),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
ss-ap: f(x),
ss-id: ss-id(),
member: t ∈ T,
all: ∀x:A. B[x]
Lemmas referenced :
top_wf
Rules used in proof :
sqequalRule,
extract_by_obid,
introduction,
hypothesis,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}x:Top. (ss-id()(x) \msim{} x)
Date html generated:
2018_07_29-AM-10_11_59
Last ObjectModification:
2018_07_04-PM-03_44_21
Theory : constructive!algebra
Home
Index