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