proposition: Lemma repeated_app_inv n x A B: repeat x n = A ++ B -> n = length A + length B /\ A = repeat x (length A) /\ B = repeat x (length B).
proof: Proof. induction n in A, B |-*. - cbn; destruct A, B; try discriminate. intuition easy. - destruct A; cbn; try discriminate. + destruct B; try discriminate. injection 1. intuition idtac. cbn; now rewrite <-H0, repeated_length. subst. cbn; now rewrite repeated_length. + injection 1; intros; edestruct IHn; eauto. intuition auto. f_equal; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)