{motive : Lean.Meta.UnificationHint → Sort u} →
  ((pattern : Lean.Meta.UnificationConstraint) →
      (constraints : List Lean.Meta.UnificationConstraint) →
        motive { pattern := pattern, constraints := constraints }) →
    (t : Lean.Meta.UnificationHint) → motive t