∀ {C : Type u_2} {D : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive]
  (motive :
    (∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact) →
      (x : CategoryTheory.ShortComplex C) → x.ShortExact → Prop)
  (x : ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact) (x_1 : CategoryTheory.ShortComplex C)
  (x_2 : x_1.ShortExact),
  (∀ (hF : ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact) (S : CategoryTheory.ShortComplex C)
      (hS : S.ShortExact), motive hF S hS) →
    motive x x_1 x_2