proposition: Lemma in_split X (a : X) (x : list X) : a el x -> exists y z, x = y ++ [a] ++ z.
proof: Proof. induction x; cbn; intros. - firstorder. - destruct H as [-> | ]. + now exists [], x. + destruct (IHx H) as (y & z & ->). now exists (a0 :: y), z. Qed.
imports: List Lia Undecidability.PCP.PCP