∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [h : CategoryTheory.Limits.HasImage f.hom] (sq : f ⟶ g) [CategoryTheory.IsIso sq],
  CategoryTheory.Limits.HasImage g.hom