proposition: Theorem Permutation_In_inv l1 l2: l1 ~p l2 -> forall x, In x l1 -> exists l, exists r, l2 = l++x::r.
proof: Proof. intros H ? ?; apply in_split, Permutation_in with (1 := H); auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)