Nuprl Lemma : subtype-value-type

[A,B:Type].  (value-type(A)) supposing (value-type(B) and (A ⊆B))


Definitions occuring in Statement :  value-type: value-type(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a value-type: value-type(T) sq_stable: SqStable(P) implies:  Q all: x:A. B[x] has-value: (a)↓ subtype_rel: A ⊆B prop: squash: T
Lemmas referenced :  sq_stable__has-value value-type-has-value equal_wf equal-wf-base base_wf value-type_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry lambdaFormation applyEquality sqequalRule independent_isectElimination dependent_functionElimination imageMemberEquality baseClosed imageElimination because_Cache isect_memberEquality axiomSqleEquality cumulativity universeEquality

\mforall{}[A,B:Type].    (value-type(A))  supposing  (value-type(B)  and  (A  \msubseteq{}r  B))

Date html generated: 2017_04_14-AM-07_15_47
Last ObjectModification: 2017_02_27-PM-02_51_00

Theory : call!by!value_1

Home Index