∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {A B X Y : CategoryTheory.Over S} (i : A ⟶ B)
  (p : X ⟶ Y) [CategoryTheory.HasLiftingProperty i.left p.left], CategoryTheory.HasLiftingProperty i p