proposition: Lemma Comp_map_congr : Congr_law Comp_map.
proof: Proof. unfold Congr_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold Comp_fun in |- *. intros a b c f g h e x. apply Pres1; auto. Qed.
imports: Category