Lemma holds_monoid_mul_rid : holds (monoid_algebra M) monoid_mul_rid. Proof. intro. change (op (α 0) (unel M) = α 0). apply runax. Qed.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Universal.EqAlgebras.