∀ {𝒮 : Type u_1} {𝒳 : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} 𝒮]
  [inst_1 : CategoryTheory.Category.{u_2, u_3} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {a b c : 𝒳} {φ : a ⟶ b}
  {ψ : b ⟶ c} {a' : 𝒳} (h : p.obj a' ⟶ R) (τ : a' ⟶ c) (π' : a' ⟶ a)
  (motive :
    p.IsHomLift h π' ∧ CategoryTheory.CategoryStruct.comp π' (CategoryTheory.CategoryStruct.comp φ ψ) = τ → Prop)
  (h_1 : p.IsHomLift h π' ∧ CategoryTheory.CategoryStruct.comp π' (CategoryTheory.CategoryStruct.comp φ ψ) = τ),
  (∀ (hπ'₁ : p.IsHomLift h π')
      (hπ'₂ : CategoryTheory.CategoryStruct.comp π' (CategoryTheory.CategoryStruct.comp φ ψ) = τ), motive ⋯) →
    motive h_1