proposition: Lemma NtH_nt_law : NT_law NtH_map.
proof: Proof. unfold NT_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold Comp_fun in |- *; simpl in |- *. unfold NtH_arrow, FunSET_mor1, FunSET_ob in |- *. intros; apply Ass. Qed.
imports: HomFunctor Ntransformation