proposition: Lemma equiv_cong2 : forall l1 l2 l, equiv l1 l2 -> equiv (l :: l1) (l :: l2).
proof: Proof. unfold equiv;intros;repeat rewrite multiplicity_of_app. auto with arith. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0