### Nuprl Lemma : equal-wf

`∀[X,Y,A:Type].  (respects-equality(Y;A) `` respects-equality(X;A) `` (∀[a:X]. ∀[b:Y].  (a = b ∈ A ∈ ℙ)))`

Proof

Definitions occuring in Statement :  respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` member: `t ∈ T` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` prop: `ℙ` member: `t ∈ T` label: `...\$L... t` guard: `{T}` respects-equality: `respects-equality(S;T)` all: `∀x:A. B[x]`
Lemmas referenced :  respects-equality_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis because_Cache Error :inhabitedIsType,  universeEquality equalityEquality dependent_functionElimination independent_functionElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}[X,Y,A:Type].    (respects-equality(Y;A)  {}\mRightarrow{}  respects-equality(X;A)  {}\mRightarrow{}  (\mforall{}[a:X].  \mforall{}[b:Y].    (a  =  b  \mmember{}  \mBbbP{})))

Date html generated: 2019_06_20-AM-11_13_47
Last ObjectModification: 2018_11_25-PM-06_16_49

Theory : core_2

Home Index