(motive : Lean.Name × Array Lean.Expr → Sort u_1) →
  (x : Lean.Name × Array Lean.Expr) →
    ((head head_1 head_2 head_3 a b : Lean.Expr) → motive (`HAdd.hAdd, #[head, head_1, head_2, head_3, a, b])) →
      ((head head_1 head_2 head_3 a b : Lean.Expr) → motive (`HMul.hMul, #[head, head_1, head_2, head_3, a, b])) →
        ((head head_1 head_2 head_3 a b : Lean.Expr) → motive (`HSub.hSub, #[head, head_1, head_2, head_3, a, b])) →
          ((head head_1 head_2 head_3 a head_4 : Lean.Expr) →
              motive (`HDiv.hDiv, #[head, head_1, head_2, head_3, a, head_4])) →
            ((head head_1 a : Lean.Expr) → motive (`Neg.neg, #[head, head_1, a])) →
              ((x : Lean.Name × Array Lean.Expr) → motive x) → motive x