proposition: Lemma eval_sum_cons : forall n a (l: mset T), (eval (sum i ((a,n)::l))) == (@Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval a)) (eval (sum i l))).
proof: Proof. intros n a [[? ? ]|[b m] l]; simpl; reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)