proposition: Lemma list_prefix_inv'' X (a : X) x u y v : ~ In a u -> ~ In a v -> x ++ a :: y = u ++ a :: v -> x = u /\ y = v.
proof: Proof. induction x in u, v |- *; intros Hu Hv H; cbn in *. - destruct u. split. reflexivity. now inversion H. inversion H; subst. cbn in Hu. tauto. - destruct u. + inversion H; subst. destruct Hv. apply in_app_iff. cbn. tauto. + inversion H; subst. eapply IHx in H2 as [-> ->]; eauto with list. Qed.
imports: Undecidability.StringRewriting.SR Setoid List Lia