∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  CategoryTheory.Presieve.IsSeparatedFor F E.presieve₀ →
    (∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j),
        CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) →
          CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows) →
      E.IsStronglySeparatedFor F