∀ {a b : CategoryTheory.Cat} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  CategoryTheory.NatTrans.toCatHom₂
      (CategoryTheory.WithTerminal.map₂ (CategoryTheory.CategoryStruct.comp η θ).toNatTrans) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithTerminal.map₂ η.toNatTrans))
      (CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithTerminal.map₂ θ.toNatTrans))