### Nuprl Lemma : strong-subtype-implies

`∀[A,B:Type].  (strong-subtype(A;B) `` {∀b:B. ∀a:A.  ((b = a ∈ B) `` (b = a ∈ A))})`

Proof

Definitions occuring in Statement :  strong-subtype: `strong-subtype(A;B)` uall: `∀[x:A]. B[x]` guard: `{T}` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` guard: `{T}` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  equal_wf exists_wf strong-subtype_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation dependent_pairFormation because_Cache hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality applyEquality productElimination sqequalRule dependent_set_memberEquality lambdaEquality dependent_functionElimination axiomEquality universeEquality isect_memberEquality

Latex:
\mforall{}[A,B:Type].    (strong-subtype(A;B)  {}\mRightarrow{}  \{\mforall{}b:B.  \mforall{}a:A.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))\})

Date html generated: 2017_04_14-AM-07_36_46
Last ObjectModification: 2017_02_27-PM-03_09_05

Theory : subtype_1

Home Index