proposition: Lemma YLpsi_arrow_map_law : Map_law0'' YLpsi_arrow.
proof: Proof. unfold Map_law0'', YLpsi_arrow in |- *. intros x y H. unfold YLpsi_map1, YLpsi_arrow1 in |- *; simpl in |- *; unfold Equal_NT in |- *; simpl in |- *. intro a0; unfold Ext in |- *; simpl in |- *; intro f. apply Pres1; assumption. Qed.
imports: HomFunctor_NT CatFunct Functor_dup1