{motive : Lean.Try.Config → Sort u} →
  (t : Lean.Try.Config) →
    ((main name targetOnly : Bool) →
        (max : ℕ) →
          (missing only harder merge wrapWithBy : Bool) →
            motive
              { main := main, name := name, targetOnly := targetOnly, max := max, missing := missing, only := only,
                harder := harder, merge := merge, wrapWithBy := wrapWithBy }) →
      motive t