{motive : Lean.Meta.Sym.Simp.Context → Sort u} →
  (t : Lean.Meta.Sym.Simp.Context) →
    ((config : Lean.Meta.Sym.Simp.Config) →
        (initialLCtxSize dischargeDepth : ℕ) →
          motive { config := config, initialLCtxSize := initialLCtxSize, dischargeDepth := dischargeDepth }) →
      motive t