(motive : Lean.Meta.Grind.AttrKind → Sort u_1) →
  (kind : Lean.Meta.Grind.AttrKind) →
    (Unit → motive (Lean.Meta.Grind.AttrKind.ematch Lean.Meta.Grind.EMatchTheoremKind.user)) →
      ((eager : Bool) → motive (Lean.Meta.Grind.AttrKind.cases eager)) →
        (Unit → motive Lean.Meta.Grind.AttrKind.intro) →
          (Unit → motive Lean.Meta.Grind.AttrKind.inj) →
            (Unit → motive Lean.Meta.Grind.AttrKind.ext) →
              ((prio : ℕ) → motive (Lean.Meta.Grind.AttrKind.symbol prio)) →
                (Unit → motive Lean.Meta.Grind.AttrKind.funCC) →
                  ((post inv : Bool) → motive (Lean.Meta.Grind.AttrKind.norm post inv)) →
                    (Unit → motive Lean.Meta.Grind.AttrKind.unfold) →
                      ((kind : Lean.Meta.Grind.EMatchTheoremKind) → motive (Lean.Meta.Grind.AttrKind.ematch kind)) →
                        (Unit → motive Lean.Meta.Grind.AttrKind.infer) → motive kind