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