∀ (motive : Option (Lean.Omega.Constraint × Lean.Omega.Coeffs) → Sort u_1) (s' : Lean.Omega.Constraint)
  (x' : Lean.Omega.Coeffs) (h_1 : Unit → motive none)
  (h_2 : (s' : Lean.Omega.Constraint) → (x' : Lean.Omega.Coeffs) → motive (some (s', x'))),
  (match some (s', x') with
    | none => h_1 ()
    | some (s', x') => h_2 s' x') =
    h_2 s' x'