proposition: Lemma YLpsi_map1_nt_law : NT_law YLpsi_map1.
proof: Proof. unfold NT_law in |- *. intros b c f; unfold YLpsi_map1, YLpsi_arrow1 in |- *; simpl in |- *. unfold Ext, FunSET_ob in |- *; intro g; simpl in |- *. unfold FunSET_mor, Comp_fun in |- *; simpl in |- *. apply (Prf_Fcomp_law F g f x). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1