(motive : Array Lean.Expr × Array (Array Bool) → Sort u_1) →
  (x : Array Lean.Expr × Array (Array Bool)) →
    ((hTypes : Array Lean.Expr) → (masks : Array (Array Bool)) → motive (hTypes, masks)) → motive x