proposition: Lemma UA_FM_diese_op_law : MonOp_law UA_FM_diese_map.
proof: Proof. unfold MonOp_law in |- *; simpl in |- *. intro l1; elim l1. simpl in |- *; intro l2. apply Trans with (UA_FM_diese_fun l2). apply Refl. apply Midl1. simpl in |- *; intros c t H l2. apply Trans with (f c +_M (UA_FM_diese_fun t +_M UA_FM_diese_fun l2)). unfold ApMop in |- *; apply Map2_l; exact (H l2). apply Mass. Qed.
imports: FunForget FreeMonoid UniversalArrow