proposition: Lemma z0 l r (H : compat_sum_unit r) : eval (sum i (run_msets (comp (merge_msets compare) l r))) == eval (sum i ((merge_msets compare) (l) (run_msets r))).
proof: Proof. unfold comp. unfold run_msets. case_eq r; intros; subst; [|reflexivity]. rewrite eval_merge_bin; auto. rewrite eval_sum_nil. apply compat_sum_unit_Unit in H. rewrite law_neutral_right. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)