{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasImages C] →
      {motive : CategoryTheory.Limits.HasImageMaps C → Sort u_1} →
        ((has_image_map : ∀ {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st) →
            motive ⋯) →
          (t : CategoryTheory.Limits.HasImageMaps C) → motive t