(motive : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr → Sort u_1) →
  (x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr) →
    ((args : Array Lean.Expr) → (fst : Array Lean.BinderInfo) → (snd : Lean.Expr) → motive (args, fst, snd)) → motive x