Nuprl Lemma : norm-pair_wf

[A:Type]. ∀[B:A ⟶ Type].
  (∀[Na:id-fun(A)]. ∀[Nb:⋂a:A. id-fun(B[a])].  (norm-pair(Na;Nb) ∈ id-fun(a:A × B[a]))) supposing 
     ((∀a:A. value-type(B[a])) and 


Definitions occuring in Statement :  norm-pair: norm-pair(Na;Nb) id-fun: id-fun(T) value-type: value-type(T) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] member: t ∈ T isect: x:A. B[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  guard: {T} and: P ∧ Q implies:  Q all: x:A. B[x] subtype_rel: A ⊆B so_apply: x[s] so_lambda: λ2x.t[x] prop: has-value: (a)↓ norm-pair: norm-pair(Na;Nb) top: Top id-fun: id-fun(T) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  value-type_wf all_wf id-fun_wf and_wf subtype_rel-equal set_wf set-value-type equal_wf value-type-has-value top_wf
Rules used in proof :  universeEquality cumulativity because_Cache axiomEquality independent_functionElimination dependent_functionElimination productEquality applyLambdaEquality independent_pairFormation dependent_set_memberEquality dependent_pairEquality rename setElimination lambdaFormation functionEquality isectEquality equalitySymmetry equalityTransitivity applyEquality lambdaEquality independent_isectElimination hypothesisEquality setEquality isectElimination callbyvalueReduce productElimination thin hypothesis extract_by_obid voidEquality voidElimination isect_memberEquality functionExtensionality sqequalRule sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    (\mforall{}[Na:id-fun(A)].  \mforall{}[Nb:\mcap{}a:A.  id-fun(B[a])].    (norm-pair(Na;Nb)  \mmember{}  id-fun(a:A  \mtimes{}  B[a])))  supposing 
          ((\mforall{}a:A.  value-type(B[a]))  and 

Date html generated: 2018_07_25-PM-01_29_53
Last ObjectModification: 2018_07_14-PM-01_22_37

Theory : call!by!value_2

Home Index