{motive : Lean.Meta.Simprocs → Sort u} →
  (t : Lean.Meta.Simprocs) →
    ((pre post : Lean.Meta.Simp.SimprocTree) →
        (simprocNames erased : Lean.PHashSet Lean.Name) →
          motive { pre := pre, post := post, simprocNames := simprocNames, erased := erased }) →
      motive t