Nuprl Lemma : bexists_cons_lemma

f,as,a,T:Top.  (∃bx(:T) ∈ [a as]. f[x] f[a] ∨b(∃bx(:T) ∈ as. f[x]))


Proof




Definitions occuring in Statement :  bexists: bexists cons: [a b] bor: p ∨bq top: Top so_apply: x[s] all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T bexists: bexists so_lambda: λ2x.t[x] top: Top so_apply: x[s] bor_mon: <𝔹,∨b> grp_op: * pi2: snd(t) pi1: fst(t) infix_ap: y
Lemmas referenced :  top_wf mon_for_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}f,as,a,T:Top.    (\mexists{}\msubb{}x(:T)  \mmember{}  [a  /  as].  f[x]  \msim{}  f[a]  \mvee{}\msubb{}(\mexists{}\msubb{}x(:T)  \mmember{}  as.  f[x]))



Date html generated: 2016_05_16-AM-07_38_10
Last ObjectModification: 2015_12_28-PM-05_44_25

Theory : list_2


Home Index