Nuprl Lemma : subtype-valueall-type

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


Definitions occuring in Statement :  valueall-type: valueall-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 valueall-type: valueall-type(T) sq_stable: SqStable(P) implies:  Q all: x:A. B[x] has-value: (a)↓ has-valueall: has-valueall(a) prop: squash: T subtype_rel: A ⊆B
Lemmas referenced :  sq_stable__has-value equal_wf equal-wf-base base_wf valueall-type_wf subtype_rel_wf valueall-type-has-valueall
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule baseApply closedConclusion baseClosed hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry because_Cache lambdaFormation dependent_functionElimination imageMemberEquality imageElimination isect_memberEquality axiomSqleEquality cumulativity universeEquality applyEquality independent_isectElimination

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

Date html generated: 2017_04_14-AM-07_15_44
Last ObjectModification: 2017_02_27-PM-02_50_56

Theory : call!by!value_1

Home Index