Library Coq.Compat.Coq817

Require Export Coq.Compat.Coq818.

Require Coq.Lists.ListSet.


Module Export Coq.
  Module Export Lists.
    Module Export ListSet.
      Import List ListSet.
      Local Lemma Private_set_diff_nodup :
        forall (A:Type) (Aeq_dec : forall x y:A, {x = y} + {x <> y}) l l',
         NoDup l -> NoDup l' -> NoDup (set_diff Aeq_dec l l').
      #[deprecated(since="8.18", note="The NoDup assumption for the second list has been dropped, please adjust uses of the lemma")]
      Notation set_diff_nodup := Private_set_diff_nodup.
    End ListSet.
  End Lists.
End Coq.