{motive : Lean.Meta.InstanceEntry → Sort u} →
  ((keys : Array Lean.Meta.InstanceKey) →
      (val : Lean.Expr) →
        (priority : ℕ) →
          (globalName? : Option Lean.Name) →
            (synthOrder : Array ℕ) →
              (attrKind : Lean.AttributeKind) →
                motive
                  { keys := keys, val := val, priority := priority, globalName? := globalName?,
                    synthOrder := synthOrder, attrKind := attrKind }) →
    (t : Lean.Meta.InstanceEntry) → motive t