∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [inst_1 : K.HasPullbacks] [P.IsStableUnderBaseChange],
  (∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y),
      (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) →
    P.IsLocalAtTarget K