proposition: Fact perm_in_head x l : In x l -> exists m, l ~p x::m.
proof: Proof. induction l as [ | y l IHl ]. + destruct 1. + intros [ ? | H ]; subst. * exists l; apply Permutation_refl. * destruct (IHl H) as (m & Hm). exists (y::m). apply Permutation_trans with (2 := perm_swap _ _ _). constructor 2; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)