proposition: Lemma z2' : forall u x, compat_prd_unit x -> eval (prd i (run_list (add_to_prd i is_unit u x))) == @Bin.value _ _ (e_bin i) (eval u) (eval (prd i (run_list x))).
proof: Proof. intros u x Hix. unfold add_to_prd. case (is_prd_spec); intros; subst. rewrite z0' by auto. rewrite eval_prd_app. reflexivity. apply is_unit_prd_Unit in H. rewrite law_neutral_left. reflexivity. rewrite z0' by auto. rewrite eval_prd_app. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)