(motive : MProd Lean.Expr (MProd (Array Bool) (Array Lean.Expr)) → Sort u_1) →
  (r : MProd Lean.Expr (MProd (Array Bool) (Array Lean.Expr))) →
    ((e : Lean.Expr) → (mask : Array Bool) → (xs : Array Lean.Expr) → motive ⟨e, mask, xs⟩) → motive r