proposition: Lemma CompV_NT_congr : Congr_law'' CompV_NT.
proof: Proof. unfold Congr_law'' in |- *; simpl in |- *. unfold Equal_NT, CompV_NT in |- *; simpl in |- *. intros F G H T1 T2 T3 eqT1_T2 a; unfold Comp_tau in |- *. apply Comp_r; apply eqT1_T2. Qed.
imports: Ntransformation Category_dup2