### Nuprl Lemma : strong-subtype-iff-respects-equality

`∀[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆r B) ∧ respects-equality(B;A))`

Proof

Definitions occuring in Statement :  strong-subtype: `strong-subtype(A;B)` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` subtype_rel: `A ⊆r B` respects-equality: `respects-equality(S;T)` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` exists: `∃x:A. B[x]`
Lemmas referenced :  strong-subtype_wf subtype_rel_wf respects-equality_wf istype-universe istype-base subtype-respects-equality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  independent_pairFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule independent_pairEquality axiomEquality hypothesis Error :lambdaEquality_alt,  dependent_functionElimination hypothesisEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  Error :universeIsType,  extract_by_obid isectElimination Error :productIsType,  instantiate universeEquality Error :lambdaFormation_alt,  Error :equalityIstype,  sqequalBase equalitySymmetry because_Cache applyEquality Error :dependent_set_memberEquality_alt,  equalityTransitivity independent_isectElimination independent_functionElimination Error :dependent_pairFormation_alt,  setElimination rename Error :setIsType,  pointwiseFunctionalityForEquality

Latex:
\mforall{}[A,B:Type].    uiff(strong-subtype(A;B);(A  \msubseteq{}r  B)  \mwedge{}  respects-equality(B;A))

Date html generated: 2019_06_20-PM-00_27_50
Last ObjectModification: 2018_11_23-PM-00_21_55

Theory : subtype_1

Home Index