∀ (uninterpretedSymbols : Std.HashSet Lean.Expr) (unusedRelevantHypotheses : Std.HashSet Lean.FVarId)
  (derivedEquations : Array (Lean.Expr × Lean.Expr)),
  sizeOf
      { uninterpretedSymbols := uninterpretedSymbols, unusedRelevantHypotheses := unusedRelevantHypotheses,
        derivedEquations := derivedEquations } =
    1 + sizeOf uninterpretedSymbols + sizeOf unusedRelevantHypotheses + sizeOf derivedEquations