Nuprl Lemma : norm-snd_wf

[A:Type]. ∀[B:A ⟶ Type].  ∀[N:⋂a:A. id-fun(B[a])]. (norm-snd(N) ∈ id-fun(a:A × B[a])) supposing ∀a:A. value-type(B[a])


Proof




Definitions occuring in Statement :  norm-snd: norm-snd(N) 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 :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a id-fun: id-fun(T) norm-snd: norm-snd(N) has-value: (a)↓ so_apply: x[s] prop: so_lambda: λ2x.t[x] subtype_rel: A ⊆B guard: {T} all: x:A. B[x] implies:  Q
Lemmas referenced :  value-type-has-value equal_wf set-value-type id-fun_wf all_wf value-type_wf set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule functionExtensionality productElimination thin callbyvalueReduce extract_by_obid isectElimination setEquality applyEquality hypothesisEquality cumulativity hypothesis independent_isectElimination lambdaEquality equalityTransitivity equalitySymmetry isectEquality functionEquality dependent_set_memberEquality dependent_pairEquality because_Cache setElimination rename productEquality axiomEquality isect_memberEquality universeEquality dependent_functionElimination lambdaFormation independent_functionElimination

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}[N:\mcap{}a:A.  id-fun(B[a])].  (norm-snd(N)  \mmember{}  id-fun(a:A  \mtimes{}  B[a]))  supposing  \mforall{}a:A.  value-type(B[a])



Date html generated: 2017_04_14-AM-07_22_08
Last ObjectModification: 2017_02_27-PM-02_55_15

Theory : call!by!value_2


Home Index