proposition: Lemma repeated_equal n y A: (forall x, x ∈ A -> x = y) -> length A = n -> repeat y n = A.
proof: Proof. induction A in n |-*; destruct n; cbn; eauto; try discriminate. injection 2. rewrite IHA; eauto. intros. erewrite <-H; intuition easy. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)