proposition: Lemma UA_FM_diese_map_law : Map_law UA_FM_diese_fun.
proof: Proof. unfold Map_law in |- *; simpl in |- *. intros l1; elim l1. intro l2; elim l2. simpl in |- *; intro; apply Refl. intros c t H1 H2; elim H2. intros c t H1 l2; elim l2. intro H2; absurd (Equal_Tlist (Concat1 c t) (Empty A)). apply Diff_Concat1_Empty. trivial. intros c0 t0 H2; simpl in |- *; intro H3; elim H3; intros H4 H5. apply Trans with (f c +_M UA_FM_diese_fun t0). unfold ApMop in |- *; apply Map2_l. apply H1; trivial. trivial. unfold ApMop in |- *; apply Map2_r. apply Pres1; trivial. Qed.
imports: FunForget FreeMonoid UniversalArrow