∀ {V : Type u_2} {G : SimpleGraph V} {α : Type u_3} {β : Type u_1} [inst : Fintype β]
  (f : (completeBipartiteGraph α β).Copy G) (x : V)
  (motive : (∃ a ∈ Finset.univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x) → Prop)
  (hr : ∃ a ∈ Finset.univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x),
  (∀ (w : β) (left : w ∈ Finset.univ) (hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w = x), motive ⋯) → motive hr