∀ {C : Type u_2} [inst : CategoryTheory.Groupoid C] {c d e : C} {p : c ⟶ d},
  p ∈ {p | CategoryTheory.Subgroupoid.Discrete.Arrows c d p} →
    ∀ {q : d ⟶ e},
      q ∈ {p | CategoryTheory.Subgroupoid.Discrete.Arrows d e p} →
        CategoryTheory.CategoryStruct.comp p q ∈ {p | CategoryTheory.Subgroupoid.Discrete.Arrows c e p}