### 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