{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.Code pu → Sort u_1) →
    (code : Lean.Compiler.LCNF.Code pu) →
      ((decl : Lean.Compiler.LCNF.LetDecl pu) →
          (k : Lean.Compiler.LCNF.Code pu) → motive (Lean.Compiler.LCNF.Code.let decl k)) →
        ((decl : Lean.Compiler.LCNF.FunDecl pu) →
            (k : Lean.Compiler.LCNF.Code pu) →
              (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.Code.fun decl k h)) →
          ((decl : Lean.Compiler.LCNF.FunDecl pu) →
              (k : Lean.Compiler.LCNF.Code pu) → motive (Lean.Compiler.LCNF.Code.jp decl k)) →
            ((fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.Code.return fvarId)) →
              ((fvarId : Lean.FVarId) →
                  (args : Array (Lean.Compiler.LCNF.Arg pu)) → motive (Lean.Compiler.LCNF.Code.jmp fvarId args)) →
                ((type : Lean.Expr) → motive (Lean.Compiler.LCNF.Code.unreach type)) →
                  ((c : Lean.Compiler.LCNF.Cases pu) → motive (Lean.Compiler.LCNF.Code.cases c)) →
                    ((fvarId : Lean.FVarId) →
                        (i offset : ℕ) →
                          (y : Lean.FVarId) →
                            (ty : Lean.Expr) →
                              (k : Lean.Compiler.LCNF.Code pu) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h)) →
                      ((fvarId : Lean.FVarId) →
                          (offset : ℕ) →
                            (y : Lean.Compiler.LCNF.Arg pu) →
                              (k : Lean.Compiler.LCNF.Code pu) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.Code.oset fvarId offset y k h)) →
                        ((fvarId : Lean.FVarId) →
                            (offset : ℕ) →
                              (y : Lean.FVarId) →
                                (k : Lean.Compiler.LCNF.Code pu) →
                                  (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                    motive (Lean.Compiler.LCNF.Code.uset fvarId offset y k h)) →
                          ((fvarId : Lean.FVarId) →
                              (cidx : ℕ) →
                                (k : Lean.Compiler.LCNF.Code pu) →
                                  (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                    motive (Lean.Compiler.LCNF.Code.setTag fvarId cidx k h)) →
                            ((fvarId : Lean.FVarId) →
                                (n : ℕ) →
                                  (check persistent : Bool) →
                                    (k : Lean.Compiler.LCNF.Code pu) →
                                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                        motive (Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h)) →
                              ((fvarId : Lean.FVarId) →
                                  (n : ℕ) →
                                    (check persistent : Bool) →
                                      (k : Lean.Compiler.LCNF.Code pu) →
                                        (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                          motive (Lean.Compiler.LCNF.Code.dec fvarId n check persistent k h)) →
                                ((fvarId : Lean.FVarId) →
                                    (k : Lean.Compiler.LCNF.Code pu) →
                                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                        motive (Lean.Compiler.LCNF.Code.del fvarId k h)) →
                                  motive code