{α : Type} →
  {motive : Lean.Meta.Grind.Order.Cnstr α → Sort u} →
    (t : Lean.Meta.Grind.Order.Cnstr α) →
      ((kind : Lean.Meta.Grind.Order.CnstrKind) →
          (u v : α) →
            (k : ℤ) →
              (e : Lean.Expr) →
                (h? : Option Lean.Expr) → motive { kind := kind, u := u, v := v, k := k, e := e, h? := h? }) →
        motive t