∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) (CategoryTheory.CategoryStruct.comp a h) =
    CategoryTheory.CategoryStruct.comp p h