{motive : Lean.Meta.Rewrites.RewriteResultConfig → Sort u} →
  ((stopAtRfl : Bool) →
      (max minHeartbeats : ℕ) →
        (goal : Lean.MVarId) →
          (target : Lean.Expr) →
            (side : Lean.Meta.Rewrites.SideConditions) →
              (mctx : Lean.MetavarContext) →
                motive
                  { stopAtRfl := stopAtRfl, max := max, minHeartbeats := minHeartbeats, goal := goal, target := target,
                    side := side, mctx := mctx }) →
    (t : Lean.Meta.Rewrites.RewriteResultConfig) → motive t