∀ (motive : Option Lean.Syntax.Range → Sort u_1) (trail : Lean.Syntax.Range)
  (h_1 : (trail : Lean.Syntax.Range) → motive (some trail)) (h_2 : (x : Option Lean.Syntax.Range) → motive x),
  (match some trail with
    | some trail => h_1 trail
    | x => h_2 x) =
    h_1 trail