### Nuprl Lemma : assert-product-deq

`∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)]. ∀[x,y:A × B].  uiff(↑(product-deq(A;B;a;b) x y);x = y ∈ (A × B))`

Proof

Definitions occuring in Statement :  product-deq: `product-deq(A;B;a;b)` deq: `EqDecider(T)` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` apply: `f a` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  product-deq: `product-deq(A;B;a;b)` proddeq: `proddeq(a;b)` pi1: `fst(t)` pi2: `snd(t)` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` deq: `EqDecider(T)` cand: `A c∧ B` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` eqof: `eqof(d)` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  assert_wf band_wf iff_transitivity eqof_wf and_wf equal_wf iff_weakening_uiff assert_of_band safe-assert-deq assert_witness product-deq_wf deq_wf pi2_wf pi1_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule productElimination thin independent_pairFormation isect_memberFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination applyEquality setElimination rename hypothesisEquality introduction addLevel independent_functionElimination because_Cache lambdaFormation independent_isectElimination productEquality independent_pairEquality lambdaEquality universeEquality isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry promote_hyp

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].  \mforall{}[x,y:A  \mtimes{}  B].
uiff(\muparrow{}(product-deq(A;B;a;b)  x  y);x  =  y)

Date html generated: 2016_05_14-AM-06_07_27
Last ObjectModification: 2015_12_26-AM-11_46_32

Theory : equality!deciders

Home Index