Nuprl Lemma : bag-member-l_eqset
[T:Type]. [L1,L2:T List]. [x:T]. uiff(x 
L1;x L2) supposing l_eqset(T;L1;L2)
Proof not projected
Definitions occuring in Statement :
l_eqset: l_eqset(T;L1;L2),
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: [x:A]. B[x],
list: type List,
universe: Type,
bag-member: x bs
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
uiff: uiff(P;Q),
bag-member: x bs,
member: t T,
and: P 
Q,
squash: T,
exists: 
x:A. B[x],
true: True,
prop: 
,
cand: A c B,
l_eqset: l_eqset(T;L1;L2),
bag: bag(T),
all: x:A. B[x],
implies: P 
Q,
guard: {T},
iff: P 
Q,
rev_implies: P Q,
subtype: S 
T
Lemmas :
member-permutation,
bag_qinc,
bag_wf,
l_member_wf,
permutation_wf,
bag-member_wf,
l_eqset_wf
\mforall{}[T:Type]. \mforall{}[L1,L2:T List]. \mforall{}[x:T]. uiff(x \mdownarrow{}\mmember{} L1;x \mdownarrow{}\mmember{} L2) supposing l\_eqset(T;L1;L2)
Date html generated:
2012_02_20-PM-05_55_24
Last ObjectModification:
2012_02_02-PM-02_29_32
Home
Index