∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ} (motive : StateTransition.Reaches f a b ∧ f b = none → Prop)
  (x : StateTransition.Reaches f a b ∧ f b = none),
  (∀ (left : StateTransition.Reaches f a b) (b0 : f b = none), motive ⋯) → motive x