∀ (coeffs : Lean.Omega.Coeffs) (constraint : Lean.Omega.Constraint)
  (justification : Lean.Elab.Tactic.Omega.Justification constraint coeffs),
  sizeOf { coeffs := coeffs, constraint := constraint, justification := justification } =
    1 + sizeOf coeffs + sizeOf constraint + sizeOf justification