proposition: Lemma eval_reduce_msets i (Idem : Idempotent R (Bin.value (e_bin i))) m : eval (sum i (reduce_mset m)) == eval (sum i m).
proof: Proof. induction m as [[a n]|[a n] m IH]. - simpl. now rewrite 2copy_idem. - simpl. rewrite IH. now rewrite 2copy_idem. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)