proposition: Lemma NT_areIso : AreNatIsos T NTinv.
proof: Proof. red in |- *; split; unfold RNatIso_law in |- *; unfold Equal_NT in |- *; simpl in |- *; unfold Comp_tau in |- *; simpl in |- *; unfold Id_CatFunct_tau in |- *; intro a. apply (Idl_inv (H a)). apply (Idr_inv (H a)). Qed.
imports: CatProperty CatFunct