proposition: Fact prefix_inv x y l ll : x::l <p y::ll -> x = y /\ l <p ll.
proof: Proof. intros (r & Hr). inversion Hr; split; auto. exists r; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)