∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId) (idx : ℕ)
  (y : Lean.FVarId) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent h)),
  (match Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_5 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_6 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent h => h_7 fvarId n check persistent h) =
    h_4 fvarId idx y h