{motive : Lean.Meta.Rewrite.Config → Sort u} →
  (t : Lean.Meta.Rewrite.Config) →
    ((transparency : Lean.Meta.TransparencyMode) →
        (offsetCnstrs : Bool) →
          (occs : Lean.Meta.Occurrences) →
            (newGoals : Lean.Meta.Rewrite.NewGoals) →
              motive
                { transparency := transparency, offsetCnstrs := offsetCnstrs, occs := occs, newGoals := newGoals }) →
      motive t