∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W =
    ⨆ J, ⨆ x, ⨆ x_1, ⨆ x_2, ⨆ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J