{motive : Lean.Elab.Tactic.SimpKind → Sort u} →
  (t : Lean.Elab.Tactic.SimpKind) →
    motive Lean.Elab.Tactic.SimpKind.simp →
      motive Lean.Elab.Tactic.SimpKind.simpAll → motive Lean.Elab.Tactic.SimpKind.dsimp → motive t