proposition: Lemma computation_eval_rw `{M:@EMonoid A E_op E_one E_eq} c : computation_eval c = computation_execute E_op c.
proof: Proof. reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)