fact: Fixpoint FG_lift_fun (p : FreeGroup) : G := match p with | Var v => f v | Law p1 p2 => sgroup_law _ (FG_lift_fun p1) (FG_lift_fun p2) | Unit => monoid_unit G | Inv p1 => group_inverse G (FG_lift_fun p1) end.
imports: Group_util