proposition: Lemma FaM_comp_prop : Equal f (comp_hom (FaM_lift:Hom (FreeAbelianMonoid:SET) M) FaM_var).
proof: Proof. simpl in |- *. red in |- *. simpl in |- *. auto with algebra. Qed.
imports: Monoid_cat Sgroup_facts Monoid_facts Monoid_util Abelian_group_facts