{motive : Lean.Meta.Grind.InjectiveTheorem → Sort u} →
  (t : Lean.Meta.Grind.InjectiveTheorem) →
    ((levelParams : Array Lean.Name) →
        (proof : Lean.Expr) →
          (symbols : List Lean.HeadIndex) →
            (origin : Lean.Meta.Grind.Origin) →
              motive { levelParams := levelParams, proof := proof, symbols := symbols, origin := origin }) →
      motive t