Nuprl Lemma : mem_nil_lemma

a,s:Top.  (a ∈b [] ff)


Proof




Definitions occuring in Statement :  mem: a ∈b as nil: [] bfalse: ff top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] mem: a ∈b as so_lambda: λ2x.t[x] member: t ∈ T top: Top so_apply: x[s] bor_mon: <𝔹,∨b> grp_id: e pi2: snd(t) pi1: fst(t)
Lemmas referenced :  mon_for_nil_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis

Latex:
\mforall{}a,s:Top.    (a  \mmember{}\msubb{}  []  \msim{}  ff)



Date html generated: 2016_05_16-AM-07_36_54
Last ObjectModification: 2015_12_28-PM-05_45_06

Theory : list_2


Home Index