∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_1}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) (K : HomologicalComplex C c)
  (motive : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0 → Prop)
  (x : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0),
  (∀ (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0), motive ⟨α, hα⟩) → motive x