proposition: Lemma Dist_map_law : Map_law Dist_fun.
proof: Proof. unfold Map_law in |- *; intros l1; elim l1. intro l2; elim l2. intros; apply Refl. intros c t H H1; elim H1. intros c t H l2; elim l2. intro H1; absurd (Equal_Tlist (Concat1 c t) (Empty A)). apply (Diff_Concat1_Empty (A:=A)). trivial. intros c0 t0 H1 H2. elim H2; intros H3 H4. simpl in |- *; split. apply Pres1; trivial. exact (H t0 H4). Qed.
imports: FreeMonoid Functor MON