{motive : Lean.Meta.Simp.Step → Sort u} →
  (t : Lean.Meta.Simp.Step) →
    ((r : Lean.Meta.Simp.Result) → motive (Lean.Meta.Simp.Step.done r)) →
      ((e : Lean.Meta.Simp.Result) → motive (Lean.Meta.Simp.Step.visit e)) →
        ((e? : Option Lean.Meta.Simp.Result) → motive (Lean.Meta.Simp.Step.continue e?)) → motive t