proposition: Lemma holds_monoid_mul_lid : holds (monoid_algebra M) monoid_mul_lid.
proof: Proof. intro. cbn in α. change (fromterm (ops (monoid_algebra M)) α tt (mul id x) = α 0). change (op (unel M) (α 0) = α 0). apply lunax. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Monoids UniMath.Algebra.Universal.EqAlgebras