∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {n : ℕ}
  (motive : G.Colorable n ∧ H.Colorable n → Prop) (x : G.Colorable n ∧ H.Colorable n),
  (∀ (cG : G.Colorable n) (cH : H.Colorable n), motive ⋯) → motive x