∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (p : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (q : F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.one),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q =
      CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.left) →
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q =
        CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.right) →
      ∀ ⦃X Y : CategoryTheory.Limits.WalkingParallelPair⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Limits.WalkingParallelPair.casesOn Y p q) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WalkingParallelPair.casesOn X p q) (G.map f)