∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s s_1 : Y ⟶ X) (e_s : s = s_1) (hs : W s),
  CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs = CategoryTheory.MorphismProperty.LeftFraction.ofInv s_1 ⋯