∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α → β) (b : β)
  (motive : (∃ a ∈ Finset.univ.val, f a = b) → Prop) (x : ∃ a ∈ Finset.univ.val, f a = b),
  (∀ (a : α) (left : a ∈ Finset.univ.val) (h : f a = b), motive ⋯) → motive x