Nuprl Lemma : id_in_bag_in_list
L:Id List. b:bag(Id). x:Id. ((L = b) 
x 
b (x L))
Proof not projected
Definitions occuring in Statement :
Id: Id,
all: x:A. B[x],
implies: P Q,
list: type List,
equal: s = t,
l_member: (x l),
bag-member: x bs,
bag: bag(T)
Lemmas :
decidable__l_member,
sq_stable_from_decidable,
bag-member-cons,
bag-member-empty-iff,
decidable__equal_Id,
cons_member,
permutation_wf,
l_member_subtype,
member_wf,
nat_wf,
l_member_wf,
Id_wf,
bag_wf,
true_wf,
squash_wf,
bag-member_wf,
rev_implies_wf,
iff_wf,
bag_qinc
\mforall{}L:Id List. \mforall{}b:bag(Id). \mforall{}x:Id. ((L = b) {}\mRightarrow{} x \mdownarrow{}\mmember{} b {}\mRightarrow{} (x \mmember{} L))
Date html generated:
2012_02_20-PM-05_55_01
Last ObjectModification:
2012_02_02-PM-02_29_20
Home
Index