(motive : List Lean.Expr → List Lean.Expr → Array Lean.Expr → Sort u_1) →
  (x x_1 : List Lean.Expr) →
    (x_2 : Array Lean.Expr) →
      ((x : Lean.Expr) →
          (xs' : List Lean.Expr) →
            (y : Lean.Expr) → (ys' : List Lean.Expr) → (eqs : Array Lean.Expr) → motive (x :: xs') (y :: ys') eqs) →
        ((x x_3 : List Lean.Expr) → (eqs : Array Lean.Expr) → motive x x_3 eqs) → motive x x_1 x_2