proposition: Lemma z1 : forall n x, eval (sum i (run_msets (return_sum i (is_unit) x n ))) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval x).
proof: Proof. intros; unfold return_sum, run_msets. case (is_sum_spec); intros; subst. - rewrite copy_mset_copy; reflexivity. - rewrite eval_sum_nil. apply copy_n_unit. auto. - reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)