∀ {n : ℕ} {α : Type u_1} {a : α} {f : Fin n → Option α}
  (motive : (∃ i, f i.rev = some a ∧ ∀ j < i, f j.rev = none) → Prop)
  (x : ∃ i, f i.rev = some a ∧ ∀ j < i, f j.rev = none),
  (∀ (i : Fin n) (h : f i.rev = some a ∧ ∀ j < i, f j.rev = none), motive ⋯) → motive x