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