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