proposition: Lemma permut_add_inside : forall a l1 l2 l3 l4, permutation (l1 ++ l2) (l3 ++ l4) -> permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
proof: Proof. unfold permutation, meq in *; intros. generalize (H a0); clear H. do 4 rewrite list_contents_app. simpl. destruct (eqA_dec a a0); simpl; auto with arith. do 2 rewrite <- plus_n_Sm; f_equal; auto. Qed.
imports: Lia Relations Multiset SetoidList