Nuprl Lemma : equality-test2
∀[A,B,C:Type].
((A = B ∈ Type)
⇒ (C = B ∈ Type)
⇒ (∀[f:A ⟶ A]. ∀[x,y,z,u,w:A]. ((x = (f y) ∈ A) ⇒ (z = (f y) ∈ A) ⇒ (w = u ∈ C) ⇒ (w = z ∈ C) ⇒ (u = x ∈ C))))
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
respects-equality: respects-equality(S;T),
all: ∀x:A. B[x]
Lemmas referenced :
respects-equality_weakening,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
Error :lambdaFormation_alt,
equalityTransitivity,
equalitySymmetry,
hypothesis,
applyEquality,
Error :lambdaEquality_alt,
hyp_replacement,
hypothesisEquality,
Error :universeIsType,
sqequalHypSubstitution,
sqequalRule,
Error :equalityIstype,
Error :inhabitedIsType,
extract_by_obid,
isectElimination,
thin,
independent_functionElimination,
dependent_functionElimination,
because_Cache,
axiomEquality,
Error :functionIsTypeImplies,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
Error :functionIsType,
instantiate,
universeEquality
Latex:
\mforall{}[A,B,C:Type].
((A = B)
{}\mRightarrow{} (C = B)
{}\mRightarrow{} (\mforall{}[f:A {}\mrightarrow{} A]. \mforall{}[x,y,z,u,w:A]. ((x = (f y)) {}\mRightarrow{} (z = (f y)) {}\mRightarrow{} (w = u) {}\mRightarrow{} (w = z) {}\mRightarrow{} (u = x))))
Date html generated:
2019_06_20-PM-01_04_14
Last ObjectModification:
2019_06_20-PM-01_02_00
Theory : core_2
Home
Index