∀ {α : Type} [inst : SizeOf α] (kind : Lean.Meta.Grind.Order.CnstrKind) (u v : α) (k : ℤ) (e : Lean.Expr)
  (h? : Option Lean.Expr),
  sizeOf { kind := kind, u := u, v := v, k := k, e := e, h? := h? } =
    1 + sizeOf kind + sizeOf u + sizeOf v + sizeOf k + sizeOf e + sizeOf h?