fact: Fixpoint FMd_lift_fun (p : FreeModule) : Mod := match p with | Var v => f v | Law p1 p2 => sgroup_law Mod (FMd_lift_fun p1) (FMd_lift_fun p2) | Unit => monoid_unit Mod | Inv p1 => group_inverse Mod (FMd_lift_fun p1) | Op a p1 => module_mult a (FMd_lift_fun p1) end.
imports: Module_util Module_facts