{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.Code pu → Sort u_1) →
    (c : 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) → motive (Lean.Compiler.LCNF.Code.jp 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)) →
            ((c : Lean.Compiler.LCNF.Cases pu) → motive (Lean.Compiler.LCNF.Code.cases c)) →
              ((fvarId : Lean.FVarId) →
                  (args : Array (Lean.Compiler.LCNF.Arg pu)) → motive (Lean.Compiler.LCNF.Code.jmp fvarId args)) →
                ((fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.Code.return fvarId)) →
                  ((type : Lean.Expr) → motive (Lean.Compiler.LCNF.Code.unreach type)) →
                    ((fv1 : Lean.FVarId) →
                        (i offset : ℕ) →
                          (fv2 : Lean.FVarId) →
                            (ty : Lean.Expr) →
                              (k : Lean.Compiler.LCNF.Code pu) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.Code.sset fv1 i offset fv2 ty k h)) →
                      ((fv1 : Lean.FVarId) →
                          (i : ℕ) →
                            (fv2 : Lean.FVarId) →
                              (k : Lean.Compiler.LCNF.Code pu) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.Code.uset fv1 i fv2 k h)) →
                        ((fvarId : Lean.FVarId) →
                            (n : ℕ) →
                              (check persistent : Bool) →
                                (k : Lean.Compiler.LCNF.Code pu) →
                                  (h :
                                      autoParam (pu = Lean.Compiler.LCNF.Purity.impure)
                                        Lean.Compiler.LCNF.Alt._auto_11) →
                                    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 :
                                        autoParam (pu = Lean.Compiler.LCNF.Purity.impure)
                                          Lean.Compiler.LCNF.Alt._auto_13) →
                                      motive (Lean.Compiler.LCNF.Code.dec fvarId n check persistent k h)) →
                            motive c