Nuprl Lemma : member-decide-assert

[x:𝔹]. (if then tt else inr x.⋅)  fi  ∈ Dec(↑x))


Proof




Definitions occuring in Statement :  assert: b ifthenelse: if then else fi  btrue: tt bool: 𝔹 decidable: Dec(P) it: uall: [x:A]. B[x] member: t ∈ T lambda: λx.A[x] inr: inr 
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B true: True prop: bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb false: False not: ¬A so_lambda: λ2x.t[x] so_apply: x[s] top: Top
Lemmas referenced :  bool_wf eqtt_to_assert it_wf subtype_rel_self equal-wf-base not_wf true_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot top_wf subtype_rel_union unit_wf2 false_wf subtype_rel_dep_function
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality hypothesis thin extract_by_obid lambdaFormation sqequalHypSubstitution unionElimination equalityElimination sqequalRule isectElimination productElimination independent_isectElimination inlEquality applyEquality intEquality baseClosed because_Cache equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination inrEquality lambdaEquality voidEquality functionEquality functionExtensionality isect_memberEquality axiomEquality

Latex:
\mforall{}[x:\mBbbB{}].  (if  x  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi    \mmember{}  Dec(\muparrow{}x))



Date html generated: 2017_04_14-AM-07_39_02
Last ObjectModification: 2017_02_27-PM-03_10_51

Theory : equality!deciders


Home Index