{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.MorphismProperty C} →
      {X Y : C} →
        {f : X ⟶ Y} →
          {motive : P.HasPushoutsAlong f → Sort u_1} →
            (t : P.HasPushoutsAlong f) →
              ((hasPushout : ∀ {W : C} (g : X ⟶ W), P g → CategoryTheory.Limits.HasPushout g f) → motive ⋯) → motive t