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