∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G₁ G₂ : StructureGroupoid H} (motive : HasGroupoid M G₁ ∧ HasGroupoid M G₂ → Prop)
  (x : HasGroupoid M G₁ ∧ HasGroupoid M G₂), (∀ (h1 : HasGroupoid M G₁) (h2 : HasGroupoid M G₂), motive ⋯) → motive x