### Nuprl Lemma : norm-pair_wf_sq

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

Proof

Definitions occuring in Statement :  norm-pair: `norm-pair(Na;Nb)` sq-id-fun: `sq-id-fun(T)` value-type: `value-type(T)` uimplies: `b supposing a` subtype_rel: `A ⊆r 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: `b supposing a` sq-id-fun: `sq-id-fun(T)` norm-pair: `norm-pair(Na;Nb)` has-value: `(a)↓` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` sq_type: `SQType(T)` implies: `P `` 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

Latex:
\mforall{}[A,B:Type].
(\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
value-type(A))

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