### Nuprl Lemma : equality-test

`∀[A,B,C:Type].  ((A = B ∈ Type) `` (C = B ∈ Type) `` (∀[x,y,z:A].  ((x = y ∈ A) `` (z = y ∈ A) `` (x = z ∈ C))))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B`
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  instantiate universeEquality equalityTransitivity equalitySymmetry applyEquality sqequalRule Error :lambdaEquality_alt,  hyp_replacement

Latex:
\mforall{}[A,B,C:Type].    ((A  =  B)  {}\mRightarrow{}  (C  =  B)  {}\mRightarrow{}  (\mforall{}[x,y,z:A].    ((x  =  y)  {}\mRightarrow{}  (z  =  y)  {}\mRightarrow{}  (x  =  z))))

Date html generated: 2019_06_20-AM-11_18_38
Last ObjectModification: 2018_09_27-PM-05_34_18

Theory : core_2

Home Index