proposition: Lemma Assoc_CatFunct : Assoc_law'' Comp_CatFunct.
proof: Proof. unfold Assoc_law'' in |- *; intros a b c f. intros T1 T2 T3. unfold Cat_comp'', Ap2'' in |- *; simpl in |- *. unfold Equal_NT, CompV_NT in |- *; simpl in |- *. intro x; unfold Comp_tau in |- *; simpl in |- *. apply Ass. Qed.
imports: Ntransformation Category_dup2