Nuprl Lemma : decide_bfalse_lemma

g,f:Top.  (case ff of inl(a) => f[a] inr(b) => g[b] g[⋅])


Definitions occuring in Statement :  bfalse: ff it: top: Top so_apply: x[s] all: x:A. B[x] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: 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

\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