∀ {M : Type u_2} {ι : Type u_1} {α : Type u_3} {f : ι → α → M} (s : Finset ι) (_g : α → M)
  (motive : (∃ a ∈ s.val, f a = _g) → Prop) (x : ∃ a ∈ s.val, f a = _g),
  (∀ (_i : ι) (hi : _i ∈ s.val) (hg : f _i = _g), motive ⋯) → motive x