∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  (R : CategoryTheory.Presieve S), R ∈ J.toPrecoverage.coverings S ↔ CategoryTheory.Sieve.generate R ∈ J S