Nuprl Lemma : l_contains-eq_set-no_repeats
[T:Type]. [as,bs:T List]. [eq:EqDecider(T)].
(no_repeats(T;as)) supposing (l_eqset(T;as;bs) and no_repeats(T;bs) and (||as|| = ||bs||))
Proof not projected
Definitions occuring in Statement :
l_eqset: l_eqset(T;L1;L2),
length: ||as||,
uimplies: b supposing a,
uall: [x:A]. B[x],
list: type List,
int: 
,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
deq: EqDecider(T)
Lemmas :
remove-repeats-length-no-repeats-iff,
rev_implies_wf,
iff_wf,
int_subtype_base,
subtype_base_sq,
l_member_wf,
set-equal_wf,
remove-repeats-set-equal,
remove-repeats-length-no-repeats,
deq_wf,
length_wf,
no_repeats_wf,
l_eqset_wf,
no_repeats_witness
\mforall{}[T:Type]. \mforall{}[as,bs:T List]. \mforall{}[eq:EqDecider(T)].
(no\_repeats(T;as)) supposing (l\_eqset(T;as;bs) and no\_repeats(T;bs) and (||as|| = ||bs||))
Date html generated:
2012_02_20-PM-05_57_58
Last ObjectModification:
2012_02_02-PM-02_30_05
Home
Index