∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (W : CategoryTheory.MorphismProperty C) (X : C)
  (i : Fin 0), W ((CategoryTheory.ComposableArrows.mk₀ X).map (CategoryTheory.homOfLE ⋯))