### Nuprl Lemma : decidable__equal_product

`∀[A:Type]. ∀[B:A ⟶ Type].`
`  ((∀a,b:A.  Dec(a = b ∈ A)) `` (∀a:A. ∀u,v:B[a].  Dec(u = v ∈ B[a])) `` (∀x,y:a:A × B[a].  Dec(x = y ∈ (a:A × B[a]))))`

Proof

Definitions occuring in Statement :  decidable: `Dec(P)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` decidable: `Dec(P)` or: `P ∨ Q` so_apply: `x[s]` prop: `ℙ` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` guard: `{T}` not: `¬A` false: `False` pi2: `snd(t)` pi1: `fst(t)` uimplies: `b supposing a`
Lemmas referenced :  all_wf decidable_wf equal_wf subtype_rel_self subtype_rel_wf not_wf equal_functionality_wrt_subtype_rel2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation productElimination thin cut hypothesis sqequalHypSubstitution dependent_functionElimination hypothesisEquality unionElimination productEquality cumulativity applyEquality functionExtensionality introduction extract_by_obid isectElimination sqequalRule lambdaEquality functionEquality universeEquality equalitySymmetry hyp_replacement Error :applyLambdaEquality,  inlFormation dependent_pairEquality inrFormation independent_functionElimination voidElimination because_Cache equalityUniverse levelHypothesis equalityTransitivity independent_isectElimination

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
((\mforall{}a,b:A.    Dec(a  =  b))  {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}u,v:B[a].    Dec(u  =  v))  {}\mRightarrow{}  (\mforall{}x,y:a:A  \mtimes{}  B[a].    Dec(x  =  y)))

Date html generated: 2016_10_21-AM-09_43_38
Last ObjectModification: 2016_07_12-AM-05_04_12

Theory : equality!deciders

Home Index