Nuprl Lemma : decidable__exists_bag-member
[T:Type]. b:bag(T). Dec(
x:T. x 
b)
Proof not projected
Definitions occuring in Statement :
decidable: Dec(P),
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
universe: Type,
bag-member: x bs,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
decidable: Dec(P),
member: t T,
or: P 
Q,
not: 
A,
implies: P 
Q,
so_lambda: 
x.t[x],
guard: {T},
nat: 
,
iff: P 
Q,
and: P 
Q,
rev_implies: P Q,
so_apply: x[s],
false: False,
prop: 
Lemmas :
decidable__lt,
bag-size_wf,
nat_wf,
bag-size-bag-member,
not_wf,
squash_wf,
exists_wf,
bag-member_wf,
bag_wf
\mforall{}[T:Type]. \mforall{}b:bag(T). Dec(\mdownarrow{}\mexists{}x:T. x \mdownarrow{}\mmember{} b)
Date html generated:
2012_01_23-PM-12_17_04
Last ObjectModification:
2012_01_18-AM-02_32_57
Home
Index