proposition: Fact In_list_repeat X (x y : X) n : In y (list_repeat x n) -> x = y /\ 0 < n.
proof: Proof. induction n; simpl; intros []. split; auto; lia. split; try lia; apply IHn; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)