(motive : Array Lean.Syntax × Array Lean.Expr → Sort u_1) →
  (x : Array Lean.Syntax × Array Lean.Expr) →
    ((binders : Array Lean.Syntax) → (fvars : Array Lean.Expr) → motive (binders, fvars)) → motive x