∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {X : C}
  {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X},
  (CategoryTheory.Presieve.ofArrows Y f ∈ P.precoverage.coverings X) = ∀ (i : ι), P (f i)