proposition: Lemma split_inv X (u z x y : list X) (s : X) : u ++ z = x ++ s :: y -> ~ s el u -> exists x' : list X, x = u ++ x'.
proof: Proof. revert u. induction x; cbn; intros. - destruct u. cbn. eauto. inv H. firstorder. - destruct u. cbn. eauto. inv H. edestruct IHx. cbn. rewrite H3. reflexivity. firstorder. subst. cbn. eauto. Qed.
imports: List Lia Undecidability.PCP.PCP