∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  (∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ S.arrows c c) →
    (∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
        γ ∈ S.arrows c c →
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p) ∈
            S.arrows d d) →
      S.IsNormal