{motive : Lean.Meta.ApplyConfig → Sort u} →
  (t : Lean.Meta.ApplyConfig) →
    ((newGoals : Lean.Meta.ApplyNewGoals) →
        (synthAssignedInstances allowSynthFailures approx : Bool) →
          motive
            { newGoals := newGoals, synthAssignedInstances := synthAssignedInstances,
              allowSynthFailures := allowSynthFailures, approx := approx }) →
      motive t