proposition: Fact is_a_head_dec (l t : list X) : { x | l = t++x } + { ~ exists x, l = t++x }.
proof: Proof. Proof using eqX_dec. revert t. induction l as [ | a l IHl ]. + intros [ | t ]. * left; exists nil; auto. * right; intros ([ | ] & ?); discriminate. + intros [ | b t ]. * left; exists (a::l); auto. * destruct (eqX_dec a b) as [ -> | C ]. - destruct (IHl t) as [ H | C ]. ++ left; destruct H as (x & ->). exists x; auto. ++ right; contradict C; destruct C as (x & E). exists x; inversion E; subst; auto. - right; contradict C; destruct C as (? & E); inversion E; auto. Qed.
imports: List Arith Lia Bool Undecidability.PCP(PCP Util.PCP_facts)