List duplicates #
Main definitions #
List.Duplicate x l : Prop
is an inductive property that holds whenx
is a duplicate inl
Implementation details #
In this file, x ∈+ l
notation is shorthand for List.Duplicate x l
.
The contrapositive of List.nodup_iff_sublist
.