proposition: Lemma comp_map_assoc : forall (A B C D : Setoid) (f : MAP A B) (g : MAP B C) (h : MAP C D), Equal (comp_map_map h (comp_map_map g f)) (comp_map_map (comp_map_map h g) f).
proof: Proof. unfold comp_map_map in |- *; simpl in |- *. unfold Map_eq in |- *; simpl in |- *; auto with algebra. Qed.