proposition: Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l ↔ List.NoDup l.
proof: Proof. split. - induction 1; constructor; rewrite <-?elem_of_list_In; auto. - induction 1; constructor; rewrite ?elem_of_list_In; auto. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)