proposition: Fact repeat_choice_two x m : Forall (eq x) m -> (exists m', m = x::x::m') \/ m = nil \/ m = x::nil.
proof: Proof. intros H. destruct m as [ | a [ | b m ] ]; auto. + inversion H; subst; auto. + rewrite Forall_forall in H. rewrite <- (H a), <- (H b); simpl; auto; left; exists m; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)