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