Nuprl Lemma : decide_bfalse_lemma
∀g,f:Top. (case ff of inl(a) => f[a] | inr(b) => g[b] ~ g[⋅])
Proof
Definitions occuring in Statement :
bfalse: ff,
it: ⋅,
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
bfalse: ff
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
hypothesis,
lemma_by_obid,
sqequalRule
Latex:
\mforall{}g,f:Top. (case ff of inl(a) => f[a] | inr(b) => g[b] \msim{} g[\mcdot{}])
Date html generated:
2016_05_15-PM-05_37_17
Last ObjectModification:
2015_12_27-PM-02_05_26
Theory : general
Home
Index