{m : Type → Type} →
  {motive : Lean.Meta.Grind.AC.MonadGetStruct m → Sort u} →
    ((getStruct : m Lean.Meta.Grind.AC.Struct) → motive { getStruct := getStruct }) →
      (t : Lean.Meta.Grind.AC.MonadGetStruct m) → motive t