{m : Type → Type} →
  {motive : Lean.Meta.MonadSimp m → Sort u} →
    (t : Lean.Meta.MonadSimp m) →
      ((withNewLemmas : {α : Type} → Array Lean.Expr → m α → m α) →
          (dsimp : Lean.Expr → m Lean.Expr) →
            (simp : Lean.Expr → m Lean.Meta.MonadSimp.Result) →
              motive { withNewLemmas := withNewLemmas, dsimp := dsimp, simp := simp }) →
        motive t