∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (out' : γ) (h_1 : (out' : γ) → motive (some out'))
  (h_2 : Unit → motive none),
  (match some out' with
    | some out' => h_1 out'
    | none => h_2 ()) =
    h_1 out'