### Nuprl Lemma : sumdeq_wf

`∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (sumdeq(a;b) ∈ (A + B) ⟶ (A + B) ⟶ 𝔹)`

Proof

Definitions occuring in Statement :  sumdeq: `sumdeq(a;b)` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  sumdeq: `sumdeq(a;b)` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` and: `P ∧ Q`
Lemmas referenced :  bfalse_wf equal_wf set_wf bool_wf all_wf iff_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaEquality hypothesisEquality equalityTransitivity hypothesis equalitySymmetry thin unionEquality lambdaFormation unionElimination applyEquality setElimination rename sqequalHypSubstitution extract_by_obid isectElimination dependent_functionElimination independent_functionElimination axiomEquality functionEquality isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].    (sumdeq(a;b)  \mmember{}  (A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbB{})

Date html generated: 2019_06_20-PM-00_32_02
Last ObjectModification: 2018_08_21-PM-01_53_07

Theory : equality!deciders

Home Index