proposition: Lemma Comp_tau_nt_law : NT_law Comp_tau.
proof: Proof. unfold Comp_tau in |- *; unfold NT_law in |- *. intros a b f. apply Trans with ((FMor F f o T b) o T' b). apply Ass. apply Trans with ((T a o FMor G f) o T' b). apply Comp_r; apply NatCond. apply Trans with (T a o FMor G f o T' b). apply Ass1. apply Trans with (T a o T' a o FMor H f). apply Comp_l; apply NatCond. apply Ass. Qed.
imports: Ntransformation Category_dup2