{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) →
    (decl : Lean.Compiler.LCNF.CodeDecl pu) →
      ((decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl)) →
        ((decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl)) →
          ((decl : Lean.Compiler.LCNF.FunDecl pu) →
              (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h)) →
            ((var : Lean.FVarId) →
                (i : ℕ) →
                  (y : Lean.FVarId) →
                    (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset var i y h)) →
              ((var : Lean.FVarId) →
                  (i offset : ℕ) →
                    (y : Lean.FVarId) →
                      (ty : Lean.Expr) →
                        (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                          motive (Lean.Compiler.LCNF.CodeDecl.sset var i offset y ty h)) →
                motive decl