### 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:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  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