proposition: Fact In_perm X (x : X) l : In x l -> exists m, x::m ~p l.
proof: Proof. intros H; apply in_split in H. destruct H as (m & k & ?); subst. exists (m++k). apply Permutation_cons_app; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)