∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} {a : C}
  (t : CategoryTheory.IsFiltered.filteredClosure f a),
  (∀ (a : C) (t : CategoryTheory.IsFiltered.filteredClosure f a),
      CategoryTheory.IsFiltered.filteredClosure.below t → motive a t) →
    motive a t