proposition: Fact prefix_list_inv l r rr : l++r <p l++rr -> r <p rr.
proof: Proof. induction l as [ | x l IHl ]; simpl; auto. intros H; apply prefix_inv, proj2, IHl in H; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)