proposition: Lemma FunFreeMon_fcomp_law : Fcomp_law FunFreeMon_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *. intros A B C f g; unfold Equal_MonMor in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intro l; elim l; simpl in |- *. trivial. intros c t H; split. apply Refl. trivial. Qed.
imports: FreeMonoid Functor MON