fact: Fixpoint FM_lift_fun (p : FreeMonoid) : M := match p with | Var v => f v | Law p1 p2 => sgroup_law _ (FM_lift_fun p1) (FM_lift_fun p2) | Unit => monoid_unit M end.
imports: Monoid_cat Sgroup_facts Monoid_facts Monoid_util