proposition: Lemma FunFreeMon_fid_law : Fid_law FunFreeMon_map.
proof: Proof. unfold Fid_law in |- *; simpl in |- *. intro A; 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