proposition: Lemma FM_comp_prop : Equal f (comp_hom (FM_lift:Hom (FreeMonoid:SET) M) FM_var).
proof: Proof. simpl in |- *. red in |- *. simpl in |- *. auto with algebra. Qed.
imports: Monoid_cat Sgroup_facts Monoid_facts Monoid_util