proposition: Lemma meq_singleton : forall a a', eqA a a' -> meq (SingletonBag a) (SingletonBag a').
proof: Proof. intros; red; simpl; intro a0. destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha; decide (Aeq_dec a' a0) with Ha; reflexivity. Qed.
imports: PeanoNat Permut Setoid