∀ (motive : (i j : CategoryTheory.Limits.WalkingPair) → i ≠ j → Sort u_1)
  (hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right)
  (h_1 :
    (hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right) →
      motive CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.WalkingPair.right hij)
  (h_2 :
    (hij : CategoryTheory.Limits.WalkingPair.right ≠ CategoryTheory.Limits.WalkingPair.left) →
      motive CategoryTheory.Limits.WalkingPair.right CategoryTheory.Limits.WalkingPair.left hij),
  (match CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right, hij with
    | CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right, hij => h_1 hij
    | CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left, hij => h_2 hij) =
    h_1 hij