∀ (self next root congr : Lean.Expr) (target? proof? : Option Lean.Expr) (flipped : Bool) (size : ℕ)
  (interpreted ctor hasLambdas heqProofs : Bool) (idx generation mt : ℕ) (sTerms : Lean.Meta.Grind.SolverTerms)
  (funCC : Bool),
  sizeOf
      { self := self, next := next, root := root, congr := congr, target? := target?, proof? := proof?,
        flipped := flipped, size := size, interpreted := interpreted, ctor := ctor, hasLambdas := hasLambdas,
        heqProofs := heqProofs, idx := idx, generation := generation, mt := mt, sTerms := sTerms, funCC := funCC } =
    1 + sizeOf self + sizeOf next + sizeOf root + sizeOf congr + sizeOf target? + sizeOf proof? + sizeOf flipped +
                        sizeOf size +
                      sizeOf interpreted +
                    sizeOf ctor +
                  sizeOf hasLambdas +
                sizeOf heqProofs +
              sizeOf idx +
            sizeOf generation +
          sizeOf mt +
        sizeOf sTerms +
      sizeOf funCC