### Nuprl Lemma : bool-to-dcdr_wf

`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[x:A].  ({f}b x ∈ Dec(f x = tt))`

Proof

Definitions occuring in Statement :  bool-to-dcdr: `{f}b` btrue: `tt` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bool-to-dcdr: `{f}b` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` prop: `ℙ`
Lemmas referenced :  bool_wf bool-to-dcdr-aux decidable_wf equal-wf-T-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry hypothesisEquality isect_memberEquality isectElimination thin because_Cache functionEquality extract_by_obid universeEquality applyEquality instantiate lambdaEquality isectEquality cumulativity baseClosed functionExtensionality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:A].    (\{f\}\msubb{}  x  \mmember{}  Dec(f  x  =  tt))

Date html generated: 2018_05_21-PM-06_29_18
Last ObjectModification: 2018_05_19-PM-04_40_13

Theory : general

Home Index