(motive : MProd (Subarray Lean.BinderInfo) (MProd (Std.Iter ℕ) (MProd Bool Lean.MessageLog)) → Sort u_1) →
  (x : MProd (Subarray Lean.BinderInfo) (MProd (Std.Iter ℕ) (MProd Bool Lean.MessageLog))) →
    ((s : Subarray Lean.BinderInfo) →
        (s_1 : Std.Iter ℕ) →
          (anyDefEqSuccess : Bool) → (messages : Lean.MessageLog) → motive ⟨s, s_1, anyDefEqSuccess, messages⟩) →
      motive x