Nuprl Lemma : strong-subtype_witness

`∀[A,B:Type].  (strong-subtype(A;B) `` (<Ax, Ax> ∈ strong-subtype(A;B)))`

Proof

Definitions occuring in Statement :  strong-subtype: `strong-subtype(A;B)` uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` pair: `<a, b>` universe: `Type` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` prop: `ℙ`
Lemmas referenced :  exists_wf equal_wf strong-subtype_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule independent_pairEquality axiomEquality lambdaEquality hypothesisEquality applyEquality sqequalHypSubstitution hypothesis productElimination thin setEquality lemma_by_obid isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A,B:Type].    (strong-subtype(A;B)  {}\mRightarrow{}  (<Ax,  Ax>  \mmember{}  strong-subtype(A;B)))

Date html generated: 2016_05_13-PM-04_10_57
Last ObjectModification: 2015_12_26-AM-11_21_43

Theory : subtype_1

Home Index