proposition: Lemma list_prefix_inv X (a : X) x u y v : ~ a el x -> ~ a el u -> x ++ a :: y = u ++ a :: v -> x = u /\ y = v.
proof: Proof. intro. revert u. induction x; intros; destruct u; inv H1; try now firstorder. eapply IHx in H4; try now firstorder. intuition congruence. Qed.
imports: List Lia Undecidability.PCP.PCP