{motive : Mathlib.Tactic.AtomM.Recurse.Context → Sort u} →
  ((ctx : Lean.Meta.Simp.Context) →
      (simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) → motive { ctx := ctx, simp := simp }) →
    (t : Mathlib.Tactic.AtomM.Recurse.Context) → motive t