{motive : Lean.Elab.Structural.IndGroupInst → Sort u} →
  (t : Lean.Elab.Structural.IndGroupInst) →
    ((toIndGroupInfo : Lean.Elab.Structural.IndGroupInfo) →
        (levels : List Lean.Level) →
          (params : Array Lean.Expr) →
            motive { toIndGroupInfo := toIndGroupInfo, levels := levels, params := params }) →
      motive t