proposition: Lemma permut_remove_hd_eq : forall l l1 l2 a b, eqA a b -> permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
proof: Proof. unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0. specialize H with a0. rewrite list_contents_app in *. simpl in *. destruct (eqA_dec a _) as [Ha|Ha]; rewrite Heq in Ha; revert H; decide (eqA_dec b a0) with Ha; lia. Qed.
imports: Lia Relations Multiset SetoidList