Nuprl Lemma : decidable__atom_equal
∀a,b:Atom. Dec(a = b ∈ Atom)
Proof
Definitions occuring in Statement :
decidable: Dec(P),
all: ∀x:A. B[x],
atom: Atom,
equal: s = t ∈ T
Definitions unfolded in proof :
decidable: Dec(P),
all: ∀x:A. B[x],
member: t ∈ T,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
false: False,
implies: P ⇒ Q,
not: ¬A
Lemmas referenced :
not_wf,
equal-wf-base,
atom_subtype_base,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
Error :lambdaFormation_alt,
Error :inhabitedIsType,
hypothesisEquality,
Error :universeIsType,
atomEquality,
introduction,
atom_eqEquality,
Error :inlEquality_alt,
axiomEquality,
hypothesis,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
baseApply,
closedConclusion,
baseClosed,
applyEquality,
Error :inrEquality_alt,
Error :isect_memberEquality_alt,
Error :lambdaEquality_alt,
universeEquality,
equalityTransitivity,
equalitySymmetry,
functionExtensionality,
independent_functionElimination,
voidElimination,
because_Cache,
Error :equalityIsType1,
dependent_functionElimination,
Error :equalityIsType4
Latex:
\mforall{}a,b:Atom. Dec(a = b)
Date html generated:
2019_06_20-AM-11_15_04
Last ObjectModification:
2018_10_06-AM-09_00_24
Theory : core_2
Home
Index