- generalize in match (H x); intro;
- generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
- simplify; fold simplify (op M);
- intro; clear H2;
- generalize in match (op_associative ? (is_semi_group ? (monoid_properties M)));
- intro;
- rewrite > H2 in H3; clear H2;