∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {X Y B : C} (f : X ⟶ B) (g : Y ⟶ B)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [CategoryTheory.IsRegularEpi g],
  CategoryTheory.IsRegularEpi (CategoryTheory.Limits.pullback.fst f g)