∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (CategoryTheory.IsSplitMono f)) {X Y : C} (f : X ⟶ Y)
  (a : CategoryTheory.IsSplitMono f)
  (motive : (∃ (a_1 : CategoryTheory.IsSplitMono (CategoryTheory.retraction f)), ⋯ = ⋯) → Prop)
  (x : ∃ (a_1 : CategoryTheory.IsSplitMono (CategoryTheory.retraction f)), ⋯ = ⋯),
  (∀ (b : CategoryTheory.IsSplitMono (CategoryTheory.retraction f)) (h : ⋯ = ⋯), motive ⋯) → motive x