proposition: Lemma Concat_congr : Map2_congr_law Concat.
proof: Proof. unfold Map2_congr_law in |- *; intro l1; elim l1. intro l2; elim l2. intros l H; apply Refl. intros c t H l3 H1; elim H1. intros c t H l2; elim l2. intros l H1; absurd (Equal_Tlist (Concat1 c t) Empty). apply Diff_Concat1_Empty. trivial. intros c0 t0 H0 l H1; elim H1; intros H2 H3. simpl in |- *; split. trivial. apply (H t0 l); trivial. Qed.
imports: Monoid