∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {x y z : C} (f : x ⟶ y)
  (g : y ⟶ z), W.multiplicativeClosure f → W g → W.multiplicativeClosure (CategoryTheory.CategoryStruct.comp f g)