∀ {pu : Lean.Compiler.LCNF.Purity} (decl decl_1 : Lean.Compiler.LCNF.FunDecl pu),
  decl = decl_1 →
    ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
      k = k_1 →
        ∀ (h : pu = Lean.Compiler.LCNF.Purity.pure),
          Lean.Compiler.LCNF.Code.fun decl k h = Lean.Compiler.LCNF.Code.fun decl_1 k_1 h