Nuprl Lemma : list-eq-in-bag-if-l_eqset-and-no_repeats
[T:Type]. [eq:EqDecider(T)]. [L1,L2:T List].
L1 = L2 supposing l_eqset(T;L1;L2) 
no_repeats(T;L1) no_repeats(T;L2)
Proof not projected
Definitions occuring in Statement :
l_eqset: l_eqset(T;L1;L2),
uimplies: b supposing a,
uall: [x:A]. B[x],
and: P Q,
list: type List,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
deq: EqDecider(T),
bag: bag(T)
Definitions :
prop: 
,
true: True,
exists: 
x:A. B[x],
squash: 
T,
cand: A c B,
member: t 
T,
bag-member: x bs,
uiff: uiff(P;Q),
bag-no-repeats: bag-no-repeats(T;bs),
uimplies: b supposing a,
all: x:A. B[x],
and: P Q,
l_eqset: l_eqset(T;L1;L2),
rev_implies: P 
Q,
iff: P 
Q,
implies: P Q,
uall: [x:A]. B[x],
subtype: S 
T,
guard: {T}
Lemmas :
deq_wf,
l_eqset_wf,
and_wf,
bag-member_wf,
bag-member-list,
no_repeats_wf,
bag_wf,
bag_qinc,
decidable-equal-deq,
bag-extensionality-no-repeats
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L1,L2:T List].
L1 = L2 supposing l\_eqset(T;L1;L2) \mwedge{} no\_repeats(T;L1) \mwedge{} no\_repeats(T;L2)
Date html generated:
2012_02_20-PM-05_55_30
Last ObjectModification:
2012_02_02-PM-02_29_35
Home
Index