∀ {X : Type u_3} [inst : TopologicalSpace X] [PolishSpace X] [inst_2 : MeasurableSpace X] [BorelSpace X] {s : Setoid X}
  [T0Space (Quotient s)] [SecondCountableTopology (Quotient s)], BorelSpace (Quotient s)