∀ {β γ : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option γ)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : γ) (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'