proposition: Lemma Ap_comp : forall (A B : Setoid) (f g : MAP A B) (x y : A), Equal x y -> Equal f g -> Equal (f x) (g y).
proof: Proof. intros A B f g x y H' H'0; try assumption. apply Trans with (f y). apply (Map_compatible_prf f); auto with algebra. simpl in H'0. unfold Map_eq in H'0. auto with algebra. Qed.