proposition: Lemma FunFreeMon_map_law : Map_law FunFreeMon_mor.
proof: Proof. unfold Map_law in |- *; simpl in |- *. intros f g; unfold Equal_MonMor in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intro H; intro l; elim l; simpl in |- *. trivial. intros c t H1; split. apply H. trivial. Qed.
imports: FreeMonoid Functor MON