proposition: Lemma permut_add_inside_eq : forall a a' l1 l2 l3 l4, eqA a a' -> permutation (l1 ++ l2) (l3 ++ l4) -> permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
proof: Proof. unfold permutation, meq in *; intros. specialize H0 with a0. repeat rewrite list_contents_app in *; simpl in *. destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha; decide (eqA_dec a' a0) with Ha; simpl; auto with arith. do 2 rewrite <- plus_n_Sm; f_equal; auto. Qed.
imports: Lia Relations Multiset SetoidList