proposition: Fact is_a_tail_dec (l t : list X) : { exists x : list X, x++t = l } + { ~ exists x : list X, x++t = l }.
proof: Proof. Proof using eqX_dec. destruct (is_a_head_dec (rev l) (rev t)) as [ H | H ]. + left; destruct H as (x & Hx). exists (rev x). apply f_equal with (f := @rev _) in Hx. rewrite rev_app_distr in Hx. do 2 rewrite rev_involutive in Hx; auto. + right; contradict H. destruct H as (x & Hx); exists (rev x); subst. apply rev_app_distr. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)