proposition: Lemma L_is_morphism: (morphism _ _ L_as_CSetoid_fun).
proof: Proof. unfold morphism. simpl. split. reflexivity. unfold Astar. intros a. induction a. simpl. reflexivity. simpl. intuition. Qed.
imports: CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid