proposition: Lemma UA_FM_law2 : UA_law2 UA_FM_mor UA_FM_diese.
proof: Proof. unfold UA_law2 in |- *; simpl in |- *. unfold UA_eq, Equal_MonMor in |- *; simpl in |- *. unfold UA_FM_diese_map, Ext in |- *; simpl in |- *. unfold Comp_fun, UA_FM_fun, FMor at 1 in |- *; simpl in |- *. intros B f h H l; elim l; simpl in |- *. apply (MMon_unit h). intros c t H1. apply Trans with (h (Concat1 c (Empty A)) +_M h t). apply (MMon_op h (Concat1 c (Empty A)) t). apply Trans with (f c +_M h t). unfold ApMop in |- *; apply Map2_r; exact (H c). unfold ApMop in |- *; apply Map2_l; trivial. Qed.
imports: FunForget FreeMonoid UniversalArrow