∀ {α : Type} {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B)
  (motive : CategoryTheory.EffectiveEpiFamily X π → Prop) (x : CategoryTheory.EffectiveEpiFamily X π),
  (∀ (x : CategoryTheory.EffectiveEpiFamily X π), motive x) → motive x