∀ (share : Lean.Meta.Sym.AlphaShareCommon.State) (maxFVar : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId))
  (proofInstInfo : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo))
  (inferType : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr)
  (getLevel : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level)
  (congrInfo : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo)
  (defEqI : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool) (debug : Bool),
  sizeOf
      { share := share, maxFVar := maxFVar, proofInstInfo := proofInstInfo, inferType := inferType,
        getLevel := getLevel, congrInfo := congrInfo, defEqI := defEqI, debug := debug } =
    1 + sizeOf share + sizeOf maxFVar + sizeOf proofInstInfo + sizeOf inferType + sizeOf getLevel + sizeOf congrInfo +
        sizeOf defEqI +
      sizeOf debug