proposition: Lemma permut_cons_eq : forall l m:list A, permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
proof: Proof. unfold permutation; simpl; intros. apply meq_trans with (munion (singletonBag a') (list_contents l)). - apply meq_left, meq_singleton; auto. - auto with datatypes. Qed.
imports: Lia Relations Multiset SetoidList