{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} →
        {X Y : C} → {x : X ⟶ Y} → W.multiplicativeClosure x → Prop