proposition: Fact not_list_has_dup_an a n : ~ list_has_dup (list_an a n).
proof: Proof. revert a; induction n as [ | n IHn ]; simpl; intros a H. + inversion H. + apply list_hd_cons_inv in H. rewrite list_an_spec in H. destruct H as [ | H ]; try lia. revert H; apply IHn. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)