∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.sset fvarId i offset y ty h) =
    1 + sizeOf fvarId + sizeOf i + sizeOf offset + sizeOf y + sizeOf ty + sizeOf h