{J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {F : CategoryTheory.Functor J (Type u_2)} →
      {motive : F.IsLocallyDirected → Sort u} →
        ((cond :
              ∀ {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
                F.map fi xi = F.map fj xj → ∃ l fli flj x, F.map fli x = xi ∧ F.map flj x = xj) →
            motive ⋯) →
          (t : F.IsLocallyDirected) → motive t