Nuprl Lemma : norm-pair_wf_sq

  (∀[Na:sq-id-fun(A)]. ∀[Nb:sq-id-fun(B)].  (norm-pair(Na;Nb) ∈ sq-id-fun(A × B))) supposing 
     ((B ⊆Base) and 
     (A ⊆Base) and 
     value-type(B) and 


Definitions occuring in Statement :  norm-pair: norm-pair(Na;Nb) sq-id-fun: sq-id-fun(T) value-type: value-type(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] member: t ∈ T product: x:A × B[x] base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq-id-fun: sq-id-fun(T) norm-pair: norm-pair(Na;Nb) has-value: (a)↓ subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] sq_type: SQType(T) implies:  Q guard: {T} prop:
Lemmas referenced :  subtype_base_sq value-type-has-value sq-id-fun_wf subtype_rel_wf base_wf value-type_wf product_subtype_base equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality independent_isectElimination hypothesis functionExtensionality productElimination sqequalRule callbyvalueReduce setEquality sqequalIntensionalEquality baseApply closedConclusion baseClosed applyEquality because_Cache productEquality axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  Error :isect_memberEquality_alt,  Error :inhabitedIsType,  universeEquality Error :dependent_set_memberEquality_alt,  independent_pairEquality Error :lambdaEquality_alt,  setElimination rename Error :lambdaFormation_alt,  dependent_functionElimination independent_functionElimination lambdaFormation

    (\mforall{}[Na:sq-id-fun(A)].  \mforall{}[Nb:sq-id-fun(B)].    (norm-pair(Na;Nb)  \mmember{}  sq-id-fun(A  \mtimes{}  B)))  supposing 
          ((B  \msubseteq{}r  Base)  and 
          (A  \msubseteq{}r  Base)  and 
          value-type(B)  and 

Date html generated: 2019_06_20-AM-11_27_23
Last ObjectModification: 2018_10_06-AM-09_00_29

Theory : call!by!value_2

Home Index