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