∀ {pu : Lean.Compiler.LCNF.Purity} (expr : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1) (expr_1 : Lean.Expr)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1),
  (Lean.Compiler.LCNF.Arg.type expr h = Lean.Compiler.LCNF.Arg.type expr_1 h_1) = (expr = expr_1)