proposition: Fact prefix_app_lft_inv X (l1 l2 m : list X) : l1++l2 <p m -> { m2 | m = l1++m2 /\ l2 <p m2 }.
proof: Proof. intros H. apply prefix_spec in H. destruct H as (r & H). exists (l2++r); simpl. solve list eq in H; split; auto. exists r; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)