∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  (H : CategoryTheory.IsPushout f g h i),
  H.IsVanKampen ↔ CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯)