{α : Type} →
  {motive : Lean.Meta.Grind.Theorems α → Sort u} →
    ((smap : Lean.PHashMap Lean.Name (List α)) →
        (origins erased : Lean.PHashSet Lean.Meta.Grind.Origin) →
          (omap : Lean.PHashMap Lean.Meta.Grind.Origin (List α)) →
            motive { smap := smap, origins := origins, erased := erased, omap := omap }) →
      (t : Lean.Meta.Grind.Theorems α) → motive t